diff --git a/algebra/Bernstein.v b/algebra/Bernstein.v index c9d86779..d232a76e 100644 --- a/algebra/Bernstein.v +++ b/algebra/Bernstein.v @@ -280,7 +280,7 @@ match v in Vector.t _ i return i <= n -> cpoly_cring R with |Vector.cons a i' v' => match n as n return (S i' <= n) -> cpoly_cring R with | O => fun p => False_rect _ (Nat.nle_succ_0 _ p) - | S n' => fun p => _C_ a[*]Bernstein (le_S_n _ _ p)[+]evalBernsteinBasisH v' (le_Sn_le _ _ p) + | S n' => fun p => _C_ a[*]Bernstein (le_S_n _ _ p)[+]evalBernsteinBasisH v' (Nat.lt_le_incl _ _ p) end end. @@ -367,7 +367,7 @@ Proof. intros H H'. replace (proj1 (Nat.lt_succ_r j n) H) with (proj1 (Nat.lt_succ_r j n) H') by apply le_irrelevent. reflexivity. - rstepl (evalBernsteinBasisH (Vector.const c i) (le_Sn_le i (S n) l)[+] + rstepl (evalBernsteinBasisH (Vector.const c i) (Nat.lt_le_incl i (S n) l)[+] _C_ c[*](Bernstein (le_S_n i n l)[+] Sum (S i) n (part_tot_nat_fun (cpoly_cring R) (S n) (fun (i0 : nat) (H : i0 < S n) => Bernstein (proj1 (Nat.lt_succ_r i0 n) H))))). replace (Bernstein (le_S_n _ _ l)) with (part_tot_nat_fun (cpoly_cring R) (S n) @@ -400,7 +400,7 @@ match v in Vector.t _ i return i <= n -> Vector.t R (S i) with | Vector.nil => fun _ => Vector.cons [0] _ Vector.nil | Vector.cons a i' v' => match n as n return S i' <= n -> Vector.t R (S (S i')) with | O => fun p => False_rect _ (Nat.nle_succ_0 _ p) - | S n' => fun p => Vector.cons (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (le_Sn_le _ _ p)) + | S n' => fun p => Vector.cons (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (Nat.lt_le_incl _ _ p)) end end. diff --git a/algebra/CPoly_ApZero.v b/algebra/CPoly_ApZero.v index fc33794f..66150ded 100644 --- a/algebra/CPoly_ApZero.v +++ b/algebra/CPoly_ApZero.v @@ -316,8 +316,8 @@ Lemma poly_01_zero : forall n i j, j <= n -> j <> i -> (poly_01 i n) ! (a_ j) [= Proof. intros. induction n0 as [| n0 Hrecn0]; intros. - rewrite <- (le_n_O_eq j H). - rewrite <- (le_n_O_eq j H) in H0. + rewrite (proj1 (Nat.le_0_r j) H). + rewrite (proj1 (Nat.le_0_r j) H) in H0. simpl in |- *. elim (eq_nat_dec i 0); intro y. rewrite y in H0. diff --git a/fta/KeyLemma.v b/fta/KeyLemma.v index c7cc3ae2..6d35d2d3 100644 --- a/fta/KeyLemma.v +++ b/fta/KeyLemma.v @@ -479,7 +479,7 @@ Proof. split. auto. intros j H9 k_j r i H10 H11. unfold k_j, r in |- *. - rewrite <- (le_n_O_eq _ H9). + rewrite (proj1 (Nat.le_0_r _) H9). replace (p3m 0) with OneR. 2: auto. astepr (a k_0[*] (t[^]k_0[*][1][^]k_0)). diff --git a/ftc/FunctSeries.v b/ftc/FunctSeries.v index ca42aa71..85c5396a 100644 --- a/ftc/FunctSeries.v +++ b/ftc/FunctSeries.v @@ -764,7 +764,7 @@ Proof. simpl in |- *; rational. auto with arith. rewrite b0; intros. - rewrite <- minus_n_n. + rewrite Nat.sub_diag. apply eq_imp_leEq. simpl in |- *; eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply mult_one. diff --git a/ftc/Partitions.v b/ftc/Partitions.v index a9e7cce4..b3a4b235 100644 --- a/ftc/Partitions.v +++ b/ftc/Partitions.v @@ -182,7 +182,7 @@ Proof. apply mult_resp_leEq_rht. apply less_leEq; apply less_plusOne. apply shift_leEq_div. - apply nring_pos; clear Hi; apply neq_O_lt; auto. + apply nring_pos; clear Hi; apply Nat.neq_0_lt_0; auto. apply shift_leEq_minus. astepl ([0][+]a). astepl a; assumption. @@ -660,7 +660,7 @@ Proof. eapply eq_transitive_unfolded. apply H. simpl in |- *; rational. - apply (lt_O_neq n); auto. + apply (Nat.neq_0_lt_0 n); auto. Qed. (** @@ -707,7 +707,7 @@ Proof. intros. apply mult_lt_compat_r. assumption. - apply neq_O_lt; auto. + apply Nat.neq_0_lt_0; auto. intros. cut (i * k <= m). intro. @@ -767,7 +767,7 @@ Proof. apply ap_irreflexive_unfolded. astepl (nring m[*]nring (R:=IR) n). apply mult_resp_ap_zero; apply Greater_imp_ap; astepl (nring (R:=IR) 0); - apply nring_less; apply neq_O_lt; auto. + apply nring_less; apply Nat.neq_0_lt_0; auto. Qed. End Even_Partitions. @@ -856,7 +856,7 @@ Lemma _Separated_imp_length_zero : forall n (P : Partition Hab n), Proof. intros n P H H0. cut (~ 0 <> n); [ auto with zarith | intro ]. - cut (0 < n); [ intro | apply neq_O_lt; auto ]. + cut (0 < n); [ intro | apply Nat.neq_0_lt_0; auto ]. cut (a [#] b). exact (eq_imp_not_ap _ _ _ H0). astepl (P _ (Nat.le_0_l _)). @@ -871,7 +871,7 @@ Lemma partition_less_imp_gt_zero : forall n (P : Partition Hab n), a [<] b -> 0 Proof. intros n P H. cut (0 <> n); intro. - apply neq_O_lt; auto. + apply Nat.neq_0_lt_0; auto. exfalso. cut (a [=] b). intro; apply less_irreflexive_unfolded with (x := a). diff --git a/ftc/RefSepRef.v b/ftc/RefSepRef.v index 82add500..323886e9 100644 --- a/ftc/RefSepRef.v +++ b/ftc/RefSepRef.v @@ -381,7 +381,7 @@ Proof. cut (0 = m); [ intro; rewrite <- H0; auto | apply RSR_HR' ]. apply partition_length_zero with Hab; rewrite <- H; apply P. elim (le_lt_dec n n); intro; simpl in |- *. - rewrite <- minus_n_n; auto. + rewrite Nat.sub_diag; auto. exfalso; apply Nat.lt_irrefl with n; auto. Qed. @@ -401,7 +401,7 @@ Proof. elim (le_lt_dec n j); intro; simpl in |- *. apply plus_lt_compat_l. apply plus_lt_reg_l with n. - repeat rewrite <- le_plus_minus; auto. + repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto. lia; auto; apply Nat.lt_trans with j; auto. elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto. elim (le_lt_dec n j); intro; simpl in |- *. @@ -416,7 +416,7 @@ Proof. cut (S (pred (m + n)) = S (pred m + n)); auto. rewrite <- plus_Sn_m. rewrite <- (Nat.lt_succ_pred 0 m); auto with arith. - apply neq_O_lt. + apply Nat.neq_0_lt_0. intro. apply Nat.lt_irrefl with 0. apply Nat.lt_trans with i; auto. @@ -572,7 +572,7 @@ Proof. cut (0 = n); [ intro; rewrite <- H0; auto | apply RSR_HP' ]. apply partition_length_zero with Hab; rewrite <- H; apply R. elim (le_lt_dec m m); intro; simpl in |- *. - rewrite <- minus_n_n; auto. + rewrite Nat.sub_diag; auto. elim (Nat.lt_irrefl _ b1). Qed. @@ -592,7 +592,7 @@ Proof. elim (le_lt_dec m j); intro; simpl in |- *. apply plus_lt_compat_l. apply plus_lt_reg_l with m. - repeat rewrite <- le_plus_minus; auto. + repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto. lia; auto; apply Nat.lt_trans with j; auto. elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto. elim (le_lt_dec m j); intro; simpl in |- *. @@ -610,7 +610,7 @@ Proof. apply Nat.lt_succ_pred with 0. apply Nat.lt_le_trans with m; auto with arith. apply Nat.lt_trans with i; auto. - apply neq_O_lt. + apply Nat.neq_0_lt_0. intro. apply Nat.lt_irrefl with 0. apply Nat.lt_trans with i; auto. diff --git a/ftc/RefSeparating.v b/ftc/RefSeparating.v index 7027e482..f682dbfa 100644 --- a/ftc/RefSeparating.v +++ b/ftc/RefSeparating.v @@ -70,7 +70,7 @@ Qed. Lemma SPap_n : n <> 0. Proof. intro. - apply (lt_O_neq n). + apply (Nat.neq_0_lt_0 n). exact RS'_pos_n. auto. Qed. @@ -221,7 +221,7 @@ Proof. exists m'. cut (m <> 0); intro. split. - cut (S m' = m); [ intro | unfold m' in |- *; apply Nat.lt_succ_pred with 0; apply neq_O_lt; + cut (S m' = m); [ intro | unfold m' in |- *; apply Nat.lt_succ_pred with 0; apply Nat.neq_0_lt_0; auto ]. rewrite H0; clear H0 m'. cut (n <= sep__part_h m). @@ -231,7 +231,7 @@ Proof. assumption. intros; apply Hm'. unfold m' in H0; rewrite <- (Nat.lt_succ_pred 0 m); auto with arith. - apply neq_O_lt; auto. + apply Nat.neq_0_lt_0; auto. apply SPap_n. rewrite H in Hm. simpl in Hm. @@ -408,7 +408,8 @@ Proof. reflexivity. exfalso. generalize b0. - apply lt_O_neq; apply RS'_pos_m. + apply Nat.neq_sym. + apply Nat.neq_0_lt_0; apply RS'_pos_m. Qed. Lemma sep__part_fun_i : diff --git a/liouville/CPoly_Euclid.v b/liouville/CPoly_Euclid.v index 99fb9872..676bb696 100644 --- a/liouville/CPoly_Euclid.v +++ b/liouville/CPoly_Euclid.v @@ -107,7 +107,7 @@ Proof. apply H; apply -> Nat.succ_lt_mono; apply H3. split; [ rewrite -> coeff_Sm_lin; destruct H0; apply H0 | unfold degree_le; intros ]. destruct m0; [ inversion H3 | simpl; destruct H0 ]. - apply H4; apply lt_S_n; apply H3. + apply H4; apply Nat.succ_lt_mono; apply H3. unfold degree_lt_pair. split; intros. unfold degree_le; intros. diff --git a/liouville/QX_root_loc.v b/liouville/QX_root_loc.v index f2f53f7b..2019dd89 100644 --- a/liouville/QX_root_loc.v +++ b/liouville/QX_root_loc.v @@ -117,7 +117,8 @@ Proof. rewrite -> nexp_ring_hom, nexp_ring_hom. rewrite <- CRings.mult_assoc, <- CRings.mult_assoc. apply mult_wdr. - rewrite (le_plus_minus _ _ Hn) at 1. + rewrite <- (Nat.sub_add _ _ Hn) at 1. + rewrite Nat.add_comm. clear H0 Hn. rewrite <- nexp_plus. rewrite -> CRings.mult_assoc. diff --git a/metric2/Compact.v b/metric2/Compact.v index 46b761c6..101f21d4 100644 --- a/metric2/Compact.v +++ b/metric2/Compact.v @@ -607,7 +607,8 @@ Proof. - intros s k d1 d2 pt Hpt e1 e2 khalf H. set (A:=Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2)) in *. set (B:=Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2)) in *. - rewrite (le_plus_minus _ _ H). + rewrite <- (Nat.sub_add _ _ H). + rewrite Nat.add_comm. assert (proj1_sig k < 1) as Y. { apply (Qle_lt_trans _ _ _ khalf). reflexivity. } assert (Y0:= (CompactTotallyBoundedStreamCauchyLemma diff --git a/model/Zmod/ZBasics.v b/model/Zmod/ZBasics.v index 6c3fb25f..966c43b2 100644 --- a/model/Zmod/ZBasics.v +++ b/model/Zmod/ZBasics.v @@ -99,7 +99,8 @@ Proof. intros k n Hle. induction k as [| k Hreck]. rewrite <- minus_n_O. - apply minus_n_n. + symmetry in |- *. + apply Nat.sub_diag. set (K := k) in |- * at 2. rewrite Hreck. unfold K in |- *; clear K. diff --git a/model/Zmod/ZDivides.v b/model/Zmod/ZDivides.v index 8d5416da..d356a926 100644 --- a/model/Zmod/ZDivides.v +++ b/model/Zmod/ZDivides.v @@ -503,10 +503,10 @@ Proof. case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *. auto with zarith. intros p q. - elim (Zdiv_eucl_POS q (Zpos p)); intros Q R. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. intros Hlt Hp HR; rewrite HR; auto with zarith. intros p q. - elim (Zdiv_eucl_POS q (Zpos p)); intros Q R. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. case R. auto with zarith. intro r'; intros H0 H1 H2. @@ -518,10 +518,10 @@ Proof. case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *. auto with zarith. intros p q. - elim (Zdiv_eucl_POS q (Zpos p)); intros Q R. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. case R; intros r' H0; intros; try (cut (Zpos r' = Zpos p); elim H0); auto with zarith. intros p q. - elim (Zdiv_eucl_POS q (Zpos p)); intros Q R. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. case R; intros; try discriminate; try tauto. Qed. @@ -536,12 +536,12 @@ Proof. case b; unfold Z.opp in |- *. auto. intro B. - elim (Zdiv_eucl_POS A (Zpos B)); intros q r. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. intro Hr; rewrite Hr; auto. intro B. generalize (Z_mod_lt (Zpos A) (Zpos B)). unfold Z.modulo, Z.div_eucl in |- *. - elim (Zdiv_eucl_POS A (Zpos B)); intros q r. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. case r. intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto. intros R Hlt HR. @@ -558,7 +558,7 @@ Proof. intro B. generalize (Z_mod_lt (Zpos A) (Zpos B)). unfold Z.modulo, Z.div_eucl in |- *. - elim (Zdiv_eucl_POS A (Zpos B)); intros q r. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. case r. intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto. intros R Hlt HR. @@ -572,7 +572,7 @@ Proof. intro B. generalize (Z_mod_lt (Zpos A) (Zpos B)). unfold Z.modulo, Z.div_eucl in |- *. - elim (Zdiv_eucl_POS A (Zpos B)); intros q r. + elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. case r. intros _ HR; fold (- q)%Z in |- *; auto. intros; discriminate. diff --git a/model/structures/Npossec.v b/model/structures/Npossec.v index 3aa427a3..3a25d649 100644 --- a/model/structures/Npossec.v +++ b/model/structures/Npossec.v @@ -82,7 +82,8 @@ Proof. cut (0 <> (x*S y0+x) -> (x*S y0+x) <> 0). intro H3. apply H3. - apply lt_O_neq. + apply Nat.neq_sym. + apply Nat.neq_0_lt_0. cut ((x*S y0+x) > 0). unfold gt in |- *. intuition. @@ -92,7 +93,7 @@ Proof. lia. lia. unfold gt in |- *. - apply neq_O_lt. + apply Nat.neq_0_lt_0. cut ((x*S y0) <> 0). auto. apply Hrecy0. diff --git a/ode/AbstractIntegration.v b/ode/AbstractIntegration.v index f87a3b25..a9bb95c2 100644 --- a/ode/AbstractIntegration.v +++ b/ode/AbstractIntegration.v @@ -460,7 +460,7 @@ Section integral_approximation. rewrite <- Qplus_assoc, <- Qmult_plus_distr_l, <- Zplus_Qplus, <- Nat2Z.inj_add. apply Qplus_le_r. change (S n * proj1_sig iw' == proj1_sig w) in A. rewrite <- A. apply Qmult_le_compat_r. rewrite <- Zle_Qle. apply inj_le. rewrite Nat.add_comm. - now apply lt_le_S. + now apply Nat.le_succ_l. apply (proj2_sig iw'). apply Qplus_le_l with (z := x), Qplus_le_l with (z := - proj1_sig w). setoid_replace (a - x + x + - proj1_sig w) with (a - proj1_sig w) by ring. diff --git a/reals/Bridges_LUB.v b/reals/Bridges_LUB.v index f97a8c83..0ae42232 100644 --- a/reals/Bridges_LUB.v +++ b/reals/Bridges_LUB.v @@ -369,8 +369,7 @@ Proof. rewrite H0. simpl in |- *. apply leEq_reflexive. - symmetry in |- *. - apply le_n_O_eq. + apply Nat.le_0_r. assumption. (* n=(S n0) *) cut ({m = S n} + {m <= n}). @@ -426,8 +425,7 @@ Proof. rewrite H0. simpl in |- *. apply leEq_reflexive. - symmetry in |- *. - apply le_n_O_eq. + apply Nat.le_0_r. assumption. (* n=(S n0) *) cut ({m = S n} + {m <= n}). @@ -561,7 +559,7 @@ Proof. apply Nat.lt_trans with (m := 3). constructor. constructor. - apply lt_S_n. + apply Nat.succ_lt_mono. assumption. simpl in |- *. algebra. @@ -646,7 +644,7 @@ Proof. apply less_transitive_unfolded with (y := nring (R:=R1) N). assumption. apply nring_less. - apply le_lt_n_Sm. + apply Nat.lt_succ_r. constructor. apply Nat.le_add_r. apply U_conversion_rate2 with (m := S (N + 3)). @@ -788,7 +786,7 @@ Proof. apply Nat.lt_trans with (m := 1). apply Nat.lt_0_succ. assumption. - case (le_lt_eq_dec 2 (S n) (lt_le_S 1 (S n) H0)). + case (le_lt_eq_dec 2 (S n) (proj1 (Nat.le_succ_l 1 (S n)) H0)). intro. cut ([1][+]nring n[*]x[<](x[+][1])[^]n). intro. @@ -800,7 +798,7 @@ Proof. apply mult_resp_pos. change (nring (R:=OF) 0[<]nring n) in |- *. apply nring_less. - apply lt_S_n. + apply Nat.succ_lt_mono. assumption. apply pos_square. apply Greater_imp_ap. @@ -816,7 +814,7 @@ Proof. simpl in |- *. apply eq_reflexive_unfolded. apply Hrecn. - apply lt_S_n. + apply Nat.succ_lt_mono. assumption. intro H1. rewrite <- H1. @@ -853,7 +851,8 @@ Proof. apply recip_resp_pos. apply pos_nring_S. apply -> Nat.succ_lt_mono. - apply neq_O_lt. + apply Nat.neq_0_lt_0. + apply Nat.neq_sym. apply (nring_ap_zero_imp R1). apply Greater_imp_ap. apply less_transitive_unfolded with (y := [1][/] x[-][1][//]H0). diff --git a/reals/Bridges_iso.v b/reals/Bridges_iso.v index 2eef18ad..d74307ae 100644 --- a/reals/Bridges_iso.v +++ b/reals/Bridges_iso.v @@ -54,7 +54,8 @@ Proof. induction n as [| n Hrecn]. exists 0. rewrite <- (plus_n_O m). - apply le_n_O_eq. + symmetry in |- *. + apply Nat.le_0_r. assumption. case (le_lt_eq_dec m (S n)). assumption. @@ -372,9 +373,9 @@ Proof. induction n as [| n Hrecn]. (* n=O *) simpl in |- *. - rewrite <- (le_n_O_eq m H1). + rewrite <- (proj1 (Nat.le_0_r m) H1). apply H0. - constructor. + apply H1. (* n=(S n0) *) simpl in |- *. case (le_lt_eq_dec m (S n)). @@ -425,9 +426,9 @@ Proof. induction n as [| n Hrecn]. (* n=O *) simpl in |- *. - rewrite <- (le_n_O_eq m H1). + rewrite <- (proj1 (Nat.le_0_r m) H1). apply H0. - constructor. + apply H1. (* n=(S n0) *) simpl in |- *. case (le_lt_eq_dec m (S n)). @@ -643,7 +644,7 @@ Proof. intros. left. intros. - rewrite <- (le_n_O_eq m H1). + rewrite (proj1 (Nat.le_0_r m) H1). assumption. intro. right. diff --git a/reals/Cauchy_CReals.v b/reals/Cauchy_CReals.v index 23e4dd9e..ed5cde9c 100644 --- a/reals/Cauchy_CReals.v +++ b/reals/Cauchy_CReals.v @@ -285,7 +285,8 @@ Proof. apply Greater_imp_ap. astepr (nring (R:=R_COrdField') n). apply nring_pos. - apply neq_O_lt. + apply Nat.neq_0_lt_0. + apply Nat.neq_sym. apply nring_ap_zero_imp with F. assumption. apply ing_nring. diff --git a/reals/IVT.v b/reals/IVT.v index d6b59d52..3662dc3c 100644 --- a/reals/IVT.v +++ b/reals/IVT.v @@ -448,7 +448,7 @@ Proof. rewrite y. simpl in |- *. rstepl (Two:IR). rstepr (Three:IR). apply less_leEq. apply two_less_three. - elim (le_lt_eq_dec _ _ (lt_le_S _ _ y)); intros H0. + elim (le_lt_eq_dec _ _ (proj1 (Nat.le_succ_l _ _) y)); intros H0. apply mult_cancel_leEq with (nring i:IR). astepl (nring 0:IR). apply nring_less. auto. apply leEq_wdl with (nring (S i) [*]Two[*] (nring i[*]Two[^]i:IR)). @@ -461,7 +461,7 @@ Proof. rstepl (nring i[*]Two[+] (Two:IR)). rstepr (nring i[*]Two[+] (nring i:IR)). apply plus_resp_leEq_lft. - elim (le_lt_eq_dec _ _ (lt_le_S _ _ H0)); intros H1. + elim (le_lt_eq_dec _ _ (proj1 (Nat.le_succ_l _ _) H0)); intros H1. apply less_leEq. apply nring_less. auto. rewrite <- H1. apply leEq_reflexive. apply less_leEq. apply mult_resp_pos. diff --git a/reals/Intervals.v b/reals/Intervals.v index 5c68c818..6362a9d6 100644 --- a/reals/Intervals.v +++ b/reals/Intervals.v @@ -893,7 +893,7 @@ Proof. apply mult_resp_nonneg. apply nring_nonneg. apply shift_leEq_div. - apply nring_pos; apply neq_O_lt; auto. + apply nring_pos; apply Nat.neq_0_lt_0; auto. apply shift_leEq_minus. rstepl a; assumption. apply shift_plus_leEq'. @@ -906,7 +906,7 @@ Proof. astepl (nring (R:=IR) i). apply nring_leEq; assumption. apply shift_leEq_div. - apply nring_pos; apply neq_O_lt; auto. + apply nring_pos; apply Nat.neq_0_lt_0; auto. apply shift_leEq_minus. rstepl a; assumption. Qed. diff --git a/reals/Q_dense.v b/reals/Q_dense.v index 24f9cc76..a375a85a 100644 --- a/reals/Q_dense.v +++ b/reals/Q_dense.v @@ -464,8 +464,7 @@ Proof. intro. rewrite H0. apply leEq_reflexive. - symmetry in |- *. - apply le_n_O_eq. + apply Nat.le_0_r. assumption. (* n=(S n0) *) cut ({m = S n} + {m <= n}). @@ -520,8 +519,7 @@ Proof. intro. rewrite H0. apply leEq_reflexive. - symmetry in |- *. - apply le_n_O_eq. + apply Nat.le_0_r. assumption. (* n=(S n0) *) cut ({m = S n} + {m <= n}). @@ -640,7 +638,7 @@ Proof. apply Nat.lt_trans with (m := 3). constructor. constructor. - apply lt_S_n. + apply Nat.succ_lt_mono. assumption. simpl in |- *. rational. @@ -716,7 +714,7 @@ Proof. apply less_transitive_unfolded with (nring (R:=Q_as_COrdField) N). assumption. apply nring_less. - apply le_lt_n_Sm. + apply Nat.lt_succ_r. constructor. apply Nat.le_add_r. apply G_conversion_rate2 with (m := S (N + 3)). @@ -869,7 +867,7 @@ Proof. apply mult_resp_less_lft. apply nring_less. apply -> Nat.succ_lt_mono. - apply le_lt_n_Sm. + apply Nat.lt_succ_r. apply Nat.le_add_r. apply shift_zero_less_minus. apply l_less_r. @@ -880,7 +878,7 @@ Proof. apply less_transitive_unfolded with (y := nring (R:=R1) N). assumption. apply nring_less. - apply le_lt_n_Sm. + apply Nat.lt_succ_r. constructor. apply mult_cancel_lft with (z := nring (R:=R1) (S N)). apply nringS_ap_zero. diff --git a/reals/Series.v b/reals/Series.v index 5bec204b..eaa7817c 100644 --- a/reals/Series.v +++ b/reals/Series.v @@ -805,14 +805,16 @@ Proof. apply AbsSmall_plus. apply HM. apply (fun p n m : nat => plus_le_reg_l n m p) with k. - rewrite <- le_plus_minus. + rewrite (Nat.add_comm k (m- k)). + rewrite Nat.sub_add. apply Nat.le_trans with (Nat.max N M + k); auto with arith. rewrite Nat.add_comm; auto with arith. apply Nat.le_trans with (S (Nat.max N M + k)); auto with arith. apply AbsSmall_minus. apply HM. apply (fun p n m : nat => plus_le_reg_l n m p) with k. - rewrite <- le_plus_minus. + rewrite (Nat.add_comm k (S (Nat.max N M + k) - k)). + rewrite Nat.sub_add. apply Nat.le_trans with (Nat.max N M + k); auto. rewrite Nat.add_comm; auto with arith. apply Nat.le_trans with (S (Nat.max N M + k)); auto with arith. @@ -894,7 +896,7 @@ Proof. assumption. auto with arith. rewrite H3. - rewrite <- minus_n_n. + rewrite Nat.sub_diag. apply eq_imp_leEq. simpl in |- *; algebra. Qed. diff --git a/reals/fast/CRcorrect.v b/reals/fast/CRcorrect.v index 7d7c2718..661edbe5 100644 --- a/reals/fast/CRcorrect.v +++ b/reals/fast/CRcorrect.v @@ -255,7 +255,7 @@ Proof. rewrite <- POS_anti_convert. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. apply inj_lt. - apply le_lt_n_Sm. + apply Nat.lt_succ_r. apply Nat.le_trans with (Nat.max n (nat_of_P ed));auto with *. change (1*P_of_succ_nat m <= en * P_of_succ_nat m)%Z. apply Zmult_lt_0_le_compat_r;auto with *. diff --git a/reals/fast/MultivariatePolynomials.v b/reals/fast/MultivariatePolynomials.v index 5d6121d3..221e201a 100644 --- a/reals/fast/MultivariatePolynomials.v +++ b/reals/fast/MultivariatePolynomials.v @@ -317,14 +317,14 @@ Proof. Qmax (MVP_apply Q_as_CRing c v0) rec) n1 b) in *. replace RHS with (R*@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) - (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) l0 (le_Sn_le _ _ l))))) (Vector.cons _ a _ v0)). + (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) l0 (Nat.lt_le_incl _ _ l))))) (Vector.cons _ a _ v0)). apply IHb. apply: mult_wdr. apply MVP_apply_wd; try reflexivity. apply Sumx_wd. intros i H. replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) l)) - with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) H (le_Sn_le n1 (S m) l))) by apply le_irrelevent. + with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) H (Nat.lt_le_incl n1 (S m) l))) by apply le_irrelevent. reflexivity. clear - Ha0 Ha1. induction n1. @@ -336,12 +336,12 @@ Proof. apply: plus_resp_nonneg. stepr (@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) - (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 l0) (le_Sn_le _ _ l))))) (Vector.cons _ a _ v0)). + (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 l0) (Nat.lt_le_incl _ _ l))))) (Vector.cons _ a _ v0)). apply IHn1. apply MVP_apply_wd; try reflexivity. apply Sumx_wd. intros i H. - replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) (le_Sn_le (S n1) (S m) l))) + replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) (Nat.lt_le_incl (S n1) (S m) l))) with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S (S n1)) (S m) (Nat.lt_lt_succ_r i (S n1) (Nat.lt_lt_succ_r i n1 H)) l)) by apply le_irrelevent. reflexivity. @@ -445,14 +445,14 @@ Proof. Qmin (MVP_apply Q_as_CRing c v0) rec) n1 b) in *. replace LHS with (R*@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) - (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) l0 (le_Sn_le _ _ l))))) (Vector.cons _ a _ v0)). + (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) l0 (Nat.lt_le_incl _ _ l))))) (Vector.cons _ a _ v0)). apply IHb. apply: mult_wdr. apply MVP_apply_wd; try reflexivity. apply Sumx_wd. intros i H. replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) l)) - with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) H (le_Sn_le n1 (S m) l))) by apply le_irrelevent. + with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) H (Nat.lt_le_incl n1 (S m) l))) by apply le_irrelevent. reflexivity. clear - Ha0 Ha1. induction n1. @@ -464,12 +464,12 @@ Proof. apply: plus_resp_nonneg. stepr (@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) - (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 l0) (le_Sn_le _ _ l))))) (Vector.cons _ a _ v0)). + (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 l0) (Nat.lt_le_incl _ _ l))))) (Vector.cons _ a _ v0)). apply IHn1. apply MVP_apply_wd; try reflexivity. apply Sumx_wd. intros i H. - replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) (le_Sn_le (S n1) (S m) l))) + replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) (Nat.lt_le_incl (S n1) (S m) l))) with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S (S n1)) (S m) (Nat.lt_lt_succ_r i (S n1) (Nat.lt_lt_succ_r i n1 H)) l)) by apply le_irrelevent. reflexivity. diff --git a/reals/fast/Plot.v b/reals/fast/Plot.v index 5ec43356..02436ee6 100644 --- a/reals/fast/Plot.v +++ b/reals/fast/Plot.v @@ -345,7 +345,7 @@ Proof. - intros. intro abs. destruct i. inversion ltni. simpl in H1. revert abs. - refine (IHn i (lt_S_n n i ltni) r step x y z d e + refine (IHn i (proj2 (Nat.succ_lt_mono n i) ltni) r step x y z d e ltde loc _ H0 H1). replace (i-n)%nat with (S i - S n)%nat by reflexivity. exact H. @@ -378,7 +378,7 @@ Proof. - intros. intro abs. destruct m. inversion ltjm. simpl in H1. - apply (IHj n m ltin (lt_S_n j m ltjm) b r stepX stepY + apply (IHj n m ltin (proj2 (Nat.succ_lt_mono j m) ltjm) b r stepX stepY d e ltde loc H H0 H1 abs). Qed. diff --git a/reals/stdlib/CMTProductIntegral.v b/reals/stdlib/CMTProductIntegral.v index c171e4e9..7eb41f98 100644 --- a/reals/stdlib/CMTProductIntegral.v +++ b/reals/stdlib/CMTProductIntegral.v @@ -593,8 +593,7 @@ Proof. 2: rewrite Nat.mul_1_l; reflexivity. intro abs. rewrite Nat.add_sub, abs, Nat.mul_0_r in H0. inversion H0. replace (i + length k)%nat with (i + 1*length k)%nat. - rewrite Nat.mod_add. reflexivity. - intro abs. rewrite Nat.add_sub, abs, Nat.mul_0_r in H0. inversion H0. + rewrite Nat.Div0.mod_add. reflexivity. rewrite Nat.mul_1_l. reflexivity. + clear IHl. simpl (list_prod (a :: l) k). rewrite app_nth1. 2: rewrite map_length; exact l0. @@ -1255,7 +1254,7 @@ Proof. pose proof (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil (kg + kf * (length (FreeSubsets (length hn)))) H2). - rewrite Nat.div_add, Nat.mod_add, Nat.div_small, Nat.mod_small in H3. + rewrite Nat.div_add, Nat.Div0.mod_add, Nat.div_small, Nat.mod_small in H3. 2: apply H0. 2: apply H0. symmetry. rewrite <- CRmult_1_r. apply CRmult_morph. rewrite <- CRmult_1_r. @@ -1289,7 +1288,6 @@ Proof. simpl. destruct H0. rewrite H4. apply ProdIntegrableSubsetRight_match. apply inuniong. exact H1. + intros abs. destruct H. rewrite abs in H. inversion H. - + intros abs. destruct H. rewrite abs in H. inversion H. - (* Other points evaluate to zero *) intros. simpl. rewrite CRmult_assoc. rewrite (CRmult_morph _ _ _ (CReq_refl _) _ 0).