80c lines

auxresults.v

@@ -288,7 +288,7 @@ Lemma set_nth_catl (i : nat) (e1 e2 : seq T) (x y : T) :
   (i < size e1)%N -> set_nth x (e1 ++ e2) i y = set_nth x e1 i y ++ e2.
 Proof.
 move: i e1 y; elim/last_ind : e2 => [i e1| e2 z ih i e1] y h; rewrite ?cats0 //.
-rewrite -rcons_cat set_nth_rcons ?size_cat ?(leq_trans h) // ?leq_addr //.       
+rewrite -rcons_cat set_nth_rcons ?size_cat ?(leq_trans h) // ?leq_addr //.
 by rewrite ih // rcons_cat //.
 Qed.
 
@@ -516,8 +516,9 @@ Qed.
 End WithEqType.
 
 Lemma subseq_nth_iota (T : eqType) (x : T) (s1 s2 : seq T) :
-  reflect (exists t, subseq t (iota 0 (size s2)) /\ s1 = [seq nth x s2 i | i <- t])
-      (subseq s1 s2).
+  reflect
+    (exists t, subseq t (iota 0 (size s2)) /\ s1 = [seq nth x s2 i | i <- t])
+    (subseq s1 s2).
 Proof.
 elim: s1 s2 => [|x1 s1 IHs1] s2/=.
   rewrite sub0seq; apply/Bool.ReflectT.
@@ -1556,7 +1557,8 @@ Qed.
 
 End MoreNumDomainTheory.
 
-Lemma sgz_prod (R : realDomainType) (I : Type) (r : seq I) (P : pred I) (F : I -> R) :
+Lemma sgz_prod (R : realDomainType) (I : Type)
+    (r : seq I) (P : pred I) (F : I -> R) :
   sgz (\prod_(x <- r | P x) F x) = \prod_(x <- r | P x) sgz (F x).
 Proof.
 elim: r => [|x r IHr]; first by rewrite !big_nil sgz1.
@@ -1596,10 +1598,16 @@ under eq_bigr => y _.
 rewrite -rmorph_prod.
 rewrite [\prod_(_ <- dec_roots _ | _) _](bigID (fun x => 0 < complex.Im x))/=.
 have im_conj: forall (z : F[i]), complex.Im z^* = - complex.Im z by case.
-have pE: map_poly Num.conj_op (map_poly (real_complex F) p) = (map_poly (real_complex F) p).
+have pE: map_poly Num.conj_op (map_poly (real_complex F) p)
+    = (map_poly (real_complex F) p).
   by rewrite -map_poly_comp; apply/eq_map_poly => z/=; rewrite oppr0.
 rewrite -[\prod_(_ <- _ | _ && ~~ _) _]big_filter.
-have iE: perm_eq [seq i <- dec_roots (map_poly (real_complex F) p) | complex.Im i != 0 & ~~ (0 < complex.Im i)] [seq x^* | x <- [seq i <- dec_roots (map_poly (real_complex F) p) | complex.Im i != 0 & (0 < complex.Im i)]].
+have iE: perm_eq
+    [seq i <- dec_roots (map_poly (real_complex F) p) |
+        complex.Im i != 0 & ~~ (0 < complex.Im i)]
+    [seq x^* |
+        x <- [seq i <- dec_roots (map_poly (real_complex F) p) |
+                complex.Im i != 0 & (0 < complex.Im i)]].
   apply/uniq_perm.
   - exact/filter_uniq/uniq_dec_roots.
   - rewrite map_inj_uniq; last exact/(inv_inj conjCK).
@@ -1655,7 +1663,8 @@ Lemma open_subspace_setT (T : topologicalType) (A : set T) :
   open (A : set (subspace setT)) = open A.
 Proof.
 rewrite !openE/=; congr (A `<=` _)%classic.
-by apply/seteqP; split; apply/subsetP => x; rewrite /interior !inE nbhs_subspaceT.
+by apply/seteqP; split; apply/subsetP => x;
+  rewrite /interior !inE nbhs_subspaceT.
 Qed.
 
 Lemma open_bigcap (T : topologicalType) (I : Type) (r : seq I) (P : pred I)
@@ -1790,8 +1799,7 @@ Lemma horner_continuous {K : numFieldType} (p : {poly K}) :
 Proof.
 apply/(eq_continuous (f:=fun x : K => \sum_(i < size p) p`_i * x ^+ i)) => x.
   by rewrite -[p in RHS]coefK horner_poly.
-apply/(@continuous_sum K
-  (GRing_regular__canonical__normedtype_PseudoMetricNormedZmod K)).
+apply/(@continuous_sum _ K^o).
 move=> /= i _.
 apply/continuousM; first exact/cst_continuous.
 exact/continuousX/id_continuous.
@@ -1804,24 +1812,24 @@ apply/(eq_continuous
     (f:=fun x : 'rV[K]_n =>
       \sum_(m <- msupp p) p@_m * \prod_i x ord0 i ^+ m i)) => x.
   exact/mevalE.
-apply/(@continuous_sum K
-  (GRing_regular__canonical__normedtype_PseudoMetricNormedZmod K)).
+apply/(@continuous_sum K K^o).
 move=> /= i _.
 apply/continuousM; first exact/cst_continuous.
 apply/continuous_prod => j _.
 exact/continuousX/coord_continuous.
 Qed.
 
-Lemma mx_continuous (T : topologicalType) (K : realFieldType) m n (f : T -> 'M[K]_(m.+1, n.+1)) :
+Lemma mx_continuous (T : topologicalType) (K : realFieldType) m n
+    (f : T -> 'M[K]_(m.+1, n.+1)) :
   (forall i j, continuous (fun x => f x i j)) ->
   continuous f.
 Proof.
 move=> fc x; apply/cvg_ballP => e e0.
 near=> y.
-rewrite -[X in X (f x)]ball_normE/= [X in X < _]mx_normrE bigmax_lt//= => -[] i j _.
-rewrite !mxE/=.
+rewrite -[X in X (f x)]ball_normE/= [X in X < _]mx_normrE bigmax_lt//=.
+move=> -[] i j _; rewrite !mxE/=.
 suff: ball (f x i j) e (f y i j).
-  by rewrite -(@ball_normE _ (GRing_regular__canonical__normedtype_PseudoMetricNormedZmod K)).
+  by rewrite -(@ball_normE _ K^o).
 move: i j.
 near: y.
 apply: filter_forall => i.
@@ -1914,7 +1922,8 @@ have ifE (x : {poly {mpoly S[n]}}): (if (i < size x)%N then x`_i else 0) = x`_i.
 by rewrite 3!ifE coefB mwidenB mulrBl.
 Qed.
 
-Lemma mcoeff_muni (A : ringType) (p : {mpoly A[n.+1]}) (i : nat) (m : 'X_{1.. n}) :
+Lemma mcoeff_muni (A : ringType) (p : {mpoly A[n.+1]})
+    (i : nat) (m : 'X_{1.. n}) :
   (muni p)`_i@_m = p@_(Multinom (rcons_tuple m i)).
 Proof.
 rewrite /muni coef_sum/= raddf_sum/=.
@@ -1926,7 +1935,8 @@ rewrite (big_neq_0 (i:=Multinom (rcons_tuple m i))) => //; first last.
   + exact/index_enum_uniq.
   rewrite mem_index_enum/= coefC eqxx mcoeffM.
   have m0: (@mdeg n 0 < (mdeg m).+1)%N by rewrite mdeg0.
-  rewrite (big_neq_0 (i:=(BMultinom m0, BMultinom (leqnn (mdeg m).+1)))) => //=; first last.
+  rewrite (big_neq_0
+    (i:=(BMultinom m0, BMultinom (leqnn (mdeg m).+1)))) => //=; first last.
   + case=> /= ul ur /eqP mE; rewrite xpair_eqE !bmeqP/= mcoeffC.
     move: mE; have [->|_ _ _] := eqVneq (bmnm ul) 0%MM.
       by rewrite add0m => <-; rewrite eqxx.
@@ -1976,13 +1986,17 @@ by rewrite coefXn eqxx mulr1 mcoeffX eqxx mulr1.
 Qed.
 
 Lemma mcoeff_mwiden (A : ringType) (p : {mpoly A[n]}) (m : 'X_{1.. n.+1}) :
-  (mwiden p)@_m = p@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))) *+ (m ord_max == 0).
+  (mwiden p)@_m
+  = p@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i))))
+    *+ (m ord_max == 0).
 Proof.
 rewrite /mwiden/= /mmap raddf_sum/=.
-rewrite (big_neq_0 (i:=(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))))); first last.
+rewrite (big_neq_0
+  (i:=(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))))); first last.
 - move=> /= u _ um.
   rewrite mul_mpolyC mcoeffZ /mmap1.
-  have ->: (\prod_(i < n) 'X_(widen_ord (leqnSn n) i) ^+ u i) = 'X_[Multinom (rcons_tuple u 0)] :> {mpoly A[n.+1]}.
+  have ->: (\prod_(i < n) 'X_(widen_ord (leqnSn n) i) ^+ u i)
+      = 'X_[Multinom (rcons_tuple u 0)] :> {mpoly A[n.+1]}.
     rewrite [RHS]mpolyXE_id big_ord_recr/= multinomE (tnth_nth 0)/= -cats1.
     rewrite nth_cat size_tuple ltnn subnn/= expr0 mulr1.
     apply/eq_bigr => i _.
@@ -2031,8 +2045,10 @@ apply/anti_leq/andP; split=> //.
 by move: (ltn_ord i); rewrite ltnS.
 Qed.
 
-Lemma mcoeff_mmulti (A : ringType) (p : {poly {mpoly A[n]}}) (m : 'X_{1.. n.+1}) :
-  (mmulti p)@_m = p`_(m ord_max)@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))).
+Lemma mcoeff_mmulti (A : ringType) (p : {poly {mpoly A[n]}})
+    (m : 'X_{1.. n.+1}) :
+  (mmulti p)@_m
+  = p`_(m ord_max)@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))).
 Proof.
 rewrite raddf_sum/=.
 rewrite (big_ord_iota _ _ xpredT
@@ -2059,7 +2075,9 @@ rewrite (big_neq_0 (i:=m ord_max)); last first.
 rewrite mem_iota/=; case: (ltnP (m ord_max) (size p)) => [mp|]; last first.
   by move=> /leq_sizeP/(_ (m ord_max) (leqnn _)) ->; rewrite mcoeff0.
 rewrite mcoeffM.
-have mm: (mdeg (mnmwiden (Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i))))) < (mdeg m).+1)%N.
+have mm:
+    (mdeg (mnmwiden (Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))))
+    < (mdeg m).+1)%N.
   rewrite ltnS !mdegE; apply/leq_sum => /= i _.
   rewrite mnmwidenE; case: (ltnP i n) => [ilt|//].
   by rewrite mnmE; move: (leqnn (m i)); congr (m _ <= _)%N; apply/val_inj.
@@ -2082,7 +2100,8 @@ have mE: m =
 rewrite (big_neq_0 (i:=(BMultinom mm, BMultinom mn))).
 - by rewrite /= -mE eqxx mem_index_enum/= mwiden_mnmwiden mcoeffXn eqxx mulr1.
 - exact/index_enum_uniq.
-case=> /= l r /eqP; rewrite mcoeffXn xpair_eqE -![_ == BMultinom _](inj_eq val_inj).
+case=> /= l r /eqP; rewrite mcoeffXn xpair_eqE
+  -![_ == BMultinom _](inj_eq val_inj).
 have [<-|i _ _] := eqVneq (U_(ord_max) *+ m ord_max)%MM r; last exact/mulr0.
 move=> mlr /negP; rewrite andbT; elim.
 apply/eqP/(@addIm _ (U_(ord_max) *+ m ord_max)%MM).