Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Source lt/le/lt_le/le_lt_trans from library. #183

Merged
merged 1 commit into from
May 13, 2023
Merged

Source lt/le/lt_le/le_lt_trans from library. #183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions algebra/COrdCauchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -214,12 +214,12 @@ Proof.
apply AbsSmall_wdl_unfolded with (Three[*]((eg[+]eg)[*]Mg)[+]Three[*]((ef[+]ef)[*]Mf)).
2: unfold eg, ef in |- *; rational.
apply AbsSmall_plus; apply AbsSmall_mult; try apply AbsSmall_plus; try apply inv_resp_AbsSmall.
apply HPf; apply le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPf; apply le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HNg; auto; apply le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPg; apply le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPg; apply le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HNf; auto; apply le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPf; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPf; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HNg; auto; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPg; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HPg; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith.
apply HNf; auto; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith.
Qed.

(**
Expand Down
2 changes: 1 addition & 1 deletion algebra/COrdFields2.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -600,7 +600,7 @@ Proof.
auto with arith.
change (nring n [<] nring (R:=R) 0) in |- *.
apply nring_less.
apply lt_le_trans with (S n).
apply Nat.lt_le_trans with (S n).
auto with arith.
exfalso. revert H; rewrite -> leEq_def. intro H; destruct H.
apply nring_less; auto with arith.
Expand Down
6 changes: 3 additions & 3 deletions algebra/CPoly_Degree.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ Lemma degree_le_mon : forall (p : RX) m n,
m <= n -> degree_le m p -> degree_le n p.
Proof.
unfold degree_le in |- *. intros. apply H0.
apply le_lt_trans with n; auto with arith.
apply Nat.le_lt_trans with n; auto with arith.
Qed.

Lemma degree_le_inv : forall (p : RX) n, degree_le n p -> degree_le n [--]p.
Expand Down Expand Up @@ -271,7 +271,7 @@ Proof.
astepl (nth_coeff m0 p[+]nth_coeff m0 q).
cut (m < m0). intro.
Step_final ([0][+] ([0]:R)).
apply lt_trans with n; auto.
apply Nat.lt_trans with n; auto.
Qed.

Lemma degree_minus_lft : forall (p q : RX) m n,
Expand All @@ -297,7 +297,7 @@ Proof.
astepl (nth_coeff m0 p[+]nth_coeff m0 q).
cut (m < m0). intro.
Step_final ([0][+] ([0]:R)).
apply lt_trans with n; auto.
apply Nat.lt_trans with n; auto.
Qed.

Lemma monic_minus : forall (p q : RX) m n,
Expand Down
36 changes: 18 additions & 18 deletions algebra/Cauchy_COF.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,8 @@ Proof.
unfold z0 in |- *; elim (HNz NN); auto; unfold NN in |- *; eauto with arith.
apply shift_minus_leEq; apply shift_leEq_plus'.
unfold cg_minus in |- *; apply shift_plus_leEq'.
elim (HNz n); auto; apply le_trans with NN; auto; unfold NN in |- *; eauto with arith.
elim (HNx n); auto; apply le_trans with NN; auto; unfold NN in |- *; eauto with arith.
elim (HNz n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith.
elim (HNx n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith.
apply shift_minus_leEq; apply shift_leEq_plus'.
unfold cg_minus in |- *; apply shift_plus_leEq'.
unfold x0 in |- *; elim (HNx NN); auto; unfold NN in |- *; eauto with arith.
Expand All @@ -133,10 +133,10 @@ Proof.
apply shift_minus_leEq; apply shift_leEq_plus'.
unfold cg_minus in |- *; apply shift_plus_leEq'.
unfold z0 in |- *; elim (HNz NN); auto; unfold NN in |- *; eauto with arith.
elim (HNz n); auto; apply le_trans with NN; auto; unfold NN in |- *; eauto with arith.
elim (HNz n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith.
apply shift_minus_leEq; apply shift_leEq_plus'.
unfold cg_minus in |- *; apply shift_plus_leEq'.
elim (HNy n); auto; apply le_trans with NN; auto; unfold NN in |- *; eauto with arith.
elim (HNy n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith.
unfold y0 in |- *; elim (HNy NN); auto; unfold NN in |- *; eauto with arith.
apply shift_minus_leEq.
rstepr (y0[-]z0).
Expand Down Expand Up @@ -378,8 +378,8 @@ Proof.
unfold KK in |- *; apply div_resp_pos; auto.
apply mult_resp_pos; auto; apply pos_three.
intros; simpl in |- *; unfold KK in |- *.
cut (N <= n); [ intro Hn | apply le_trans with (max N Ny); auto with arith ].
cut (Ny <= n); [ intro Hn' | apply le_trans with (max N Ny); auto with arith ].
cut (N <= n); [ intro Hn | apply Nat.le_trans with (max N Ny); auto with arith ].
cut (Ny <= n); [ intro Hn' | apply Nat.le_trans with (max N Ny); auto with arith ].
apply leEq_transitive with (e[/] _[//]pos_ap_zero _ _ (Hy' n Hn')).
apply mult_cancel_leEq with ([1][/] _[//]pos_ap_zero _ _ He).
apply recip_resp_pos; auto.
Expand All @@ -402,8 +402,8 @@ Proof.
unfold KK in |- *; apply div_resp_pos; auto.
apply mult_resp_pos; auto; apply pos_three.
intros; simpl in |- *; unfold KK in |- *.
cut (N <= n); [ intro Hn | apply le_trans with (max N Ny); auto with arith ].
cut (Ny <= n); [ intro Hn' | apply le_trans with (max N Ny); auto with arith ].
cut (N <= n); [ intro Hn | apply Nat.le_trans with (max N Ny); auto with arith ].
cut (Ny <= n); [ intro Hn' | apply Nat.le_trans with (max N Ny); auto with arith ].
apply leEq_transitive with (e[/] _[//]pos_ap_zero _ _ (Hy' n Hn')).
apply mult_cancel_leEq with ([1][/] _[//]pos_ap_zero _ _ He).
apply recip_resp_pos; auto.
Expand Down Expand Up @@ -885,19 +885,19 @@ Proof.
rstepr (x_ m[-]x_ N1[+] (x_ N1[-]x_ m0)).
apply AbsSmall_plus.
apply px2.
apply le_trans with NN; assumption.
apply Nat.le_trans with NN; assumption.
apply AbsSmall_minus.
apply px2.
apply le_trans with NN; assumption.
apply Nat.le_trans with NN; assumption.
unfold e8 in |- *.
rstepl (e [/]SixteenNZ[+]e [/]SixteenNZ).
rstepr (y_ m0[-]y_ N2[+] (y_ N2[-]y_ m)).
apply AbsSmall_plus.
apply py2.
apply le_trans with NN; assumption.
apply Nat.le_trans with NN; assumption.
apply AbsSmall_minus.
apply py2.
apply le_trans with NN; assumption.
apply Nat.le_trans with NN; assumption.
Qed.

Lemma R_ap_alt_2 : forall x y : R_CSetoid, {e : F | [0] [<] e |
Expand Down Expand Up @@ -927,9 +927,9 @@ Proof.
assert (N_NN : N <= NN).
unfold NN in |- *; auto with arith.
assert (N1_NN : N1 <= NN).
unfold NN in |- *; apply le_trans with (max N1 N2); auto with arith.
unfold NN in |- *; apply Nat.le_trans with (max N1 N2); auto with arith.
assert (N2_NN : N2 <= NN).
unfold NN in |- *; apply le_trans with (max N1 N2); auto with arith.
unfold NN in |- *; apply Nat.le_trans with (max N1 N2); auto with arith.
set (x0 := x_ NN) in *.
set (y0 := y_ NN) in *.
simpl in |- *.
Expand Down Expand Up @@ -961,7 +961,7 @@ Proof.
rstepr (x_ m[-]x_ N1[+] (x_ N1[-]x0)).
apply plus_resp_leEq_both.
assert (H7 : AbsSmall e16 (x_ m[-]x_ N1)).
apply H31; apply le_trans with NN; auto.
apply H31; apply Nat.le_trans with NN; auto.
elim H7; intros.
rstepl ([--]e16).
assumption.
Expand All @@ -986,7 +986,7 @@ Proof.
assert (H7 : AbsSmall e16 (y_ N2[-]y_ m)).
apply AbsSmall_minus.
apply H41.
apply le_trans with NN; auto.
apply Nat.le_trans with NN; auto.
elim H7; intros.
rstepl ([--]e16).
assumption.
Expand All @@ -1006,7 +1006,7 @@ Proof.
apply plus_resp_leEq_both.
assert (H8 : AbsSmall e16 (y_ m[-]y_ N2)).
apply H41.
apply le_trans with NN; auto.
apply Nat.le_trans with NN; auto.
elim H8; intros.
rstepl ([--]e16).
assumption.
Expand All @@ -1033,7 +1033,7 @@ Proof.
assert (H8 : AbsSmall e16 (x_ N1[-]x_ m)).
apply AbsSmall_minus.
apply H31.
apply le_trans with NN; auto.
apply Nat.le_trans with NN; auto.
elim H8; intros.
rstepl ([--]e16).
assumption.
Expand Down
6 changes: 3 additions & 3 deletions fta/KeyLemma.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ Proof.
apply less_leEq; apply a_0_eps_fuzz.
intros l H H0.
cut (1 <= n - j). intro H1.
2: apply le_trans with (n - S j); [ auto | apply lem_1b ].
2: apply Nat.le_trans with (n - S j); [ auto | apply lem_1b ].
cut (n - j <= n). intro H2.
2: apply lem_1c.
elim (Hrecj H1 H2). intros t' H4 H5.
Expand Down Expand Up @@ -184,7 +184,7 @@ Proof.
auto.
exists k'.
split.
apply le_trans with (n - j).
apply Nat.le_trans with (n - j).
unfold l in |- *; apply lem_1b.
auto.
split. auto.
Expand Down Expand Up @@ -502,7 +502,7 @@ Proof.
exists (chfun k' k_SJ J).
split. intro i.
apply chfun_3. auto. auto.
apply le_trans with (k' J); auto.
apply Nat.le_trans with (k' J); auto.
elim (H10 J). auto.
split.
intro i. apply chfun_4; auto.
Expand Down
4 changes: 2 additions & 2 deletions fta/MainLemma.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ Proof.
rstepl (a i[*] (r[^]i[*]Three[^]i) [-]eps).
astepl (a i[*] (r[*]Three) [^]i[-]eps).
apply H2; auto with arith.
apply le_trans with (S k); auto.
apply Nat.le_trans with (S k); auto.
astepl (Sum (S k) n (fun i : nat => (a k[*] (r[*]Three) [^]k[+]eps) [*][1][/] Three[^]i[//]H3 i)).
astepl (Sum (S k) n (fun i : nat => (a k[*] (r[*]Three) [^]k[+]eps) [*] ([1][/] Three[^]i[//]H3 i))).
apply leEq_wdl with ((a k[*] (r[*]Three) [^]k[+]eps) [*]
Expand Down Expand Up @@ -463,7 +463,7 @@ Proof.
intros i0 H17 H18.
rewrite <- H12.
apply H8; auto with arith.
apply le_trans with (S j); auto with arith.
apply Nat.le_trans with (S j); auto with arith.
split.
astepl ([1][*] (t[*]p3m (S j)) [^]n).
astepl (a n[*] (t[*]p3m (S j)) [^]n).
Expand Down
4 changes: 2 additions & 2 deletions ftc/COrdLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -348,15 +348,15 @@ Proof.
elim (le_lt_dec (f (S n)) i); intro; simpl in |- *.
cut (f n < f (S n)); [ intro | apply f_mon; apply lt_n_Sn ].
exfalso; apply (le_not_lt (f n) i); auto.
apply le_trans with (f (S n)); auto with arith.
apply Nat.le_trans with (f (S n)); auto with arith.
intros; unfold part_tot_nat_fun in |- *;
elim (le_lt_dec (f (S n)) i);elim (le_lt_dec (f n) i);simpl;intros; try reflexivity;try exfalso; try lia.
rewrite <-H1; cut (0 < f (S n)); [ intro | rewrite <- f0; auto with arith ];
cut (f (S n) = S (pred (f (S n)))); [ intro | apply S_pred with 0; auto ];
rewrite <- H3; apply lt_le_weak; auto with arith.
intros; unfold part_tot_nat_fun in |- *;elim (le_lt_dec (f (S n)) i);
[intro; simpl in |- *; exfalso; lia| reflexivity].
apply lt_trans with (f n); auto with arith.
apply Nat.lt_trans with (f n); auto with arith.
red in |- *; intros; rewrite -> H1; reflexivity.
Qed.

Expand Down
4 changes: 2 additions & 2 deletions ftc/Composition.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -479,9 +479,9 @@ Proof.
exists (max N M).
intros n Hn x Hx.
assert (Hn0 : N <= n).
apply le_trans with (max N M); auto with *.
apply Nat.le_trans with (max N M); auto with *.
assert (Hn1 : M <= n).
apply le_trans with (max N M); auto with *.
apply Nat.le_trans with (max N M); auto with *.
apply AbsSmall_imp_AbsIR.
assert (X:Continuous_I (a:=a) (b:=b) Hab (G[o]f n)).
eapply Continuous_I_comp.
Expand Down
16 changes: 8 additions & 8 deletions ftc/FunctSequence.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -816,8 +816,8 @@ Proof.
eapply leEq_transitive.
apply triangle_IR.
apply plus_resp_leEq_both.
unfold incf in |- *; apply HNf; apply le_trans with (max Nf Ng); auto.
unfold incg in |- *; apply HNg; apply le_trans with (max Nf Ng); auto.
unfold incf in |- *; apply HNf; apply Nat.le_trans with (max Nf Ng); auto.
unfold incg in |- *; apply HNg; apply Nat.le_trans with (max Nf Ng); auto.
Qed.

Lemma fun_Lim_seq_minus' : forall H H',
Expand All @@ -839,8 +839,8 @@ Proof.
eapply leEq_transitive.
apply triangle_IR_minus.
apply plus_resp_leEq_both.
unfold incf in |- *; apply HNf; apply le_trans with (max Nf Ng); auto.
unfold incg in |- *; apply HNg; apply le_trans with (max Nf Ng); auto.
unfold incf in |- *; apply HNf; apply Nat.le_trans with (max Nf Ng); auto.
unfold incg in |- *; apply HNg; apply Nat.le_trans with (max Nf Ng); auto.
Qed.

Lemma fun_Lim_seq_mult' : forall H H',
Expand Down Expand Up @@ -891,22 +891,22 @@ Proof.
apply AbsIR_nonneg.
eapply shift_mult_leEq'.
apply pos_max_one.
unfold eg in HNG; unfold incg in |- *; apply HNG; apply le_trans with (max NF NG); auto.
unfold eg in HNG; unfold incg in |- *; apply HNG; apply Nat.le_trans with (max NF NG); auto.
eapply leEq_wdl.
2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
apply leEq_transitive with (ee [/]ThreeNZ[*]ee [/]ThreeNZ).
2: astepr (ee [/]ThreeNZ[*][1]); apply mult_resp_leEq_lft.
apply mult_resp_leEq_both; try apply AbsIR_nonneg.
eapply leEq_transitive.
unfold incf in |- *; apply HNF; apply le_trans with (max NF NG); auto.
unfold incf in |- *; apply HNF; apply Nat.le_trans with (max NF NG); auto.
unfold ef in |- *.
apply shift_div_leEq.
apply pos_max_one.
astepl (ee [/]ThreeNZ[*][1]); apply mult_resp_leEq_lft.
apply rht_leEq_Max.
apply less_leEq; apply shift_less_div; astepl ZeroR; [ apply pos_three | assumption ].
eapply leEq_transitive.
unfold incg in |- *; apply HNG; apply le_trans with (max NF NG); auto.
unfold incg in |- *; apply HNG; apply Nat.le_trans with (max NF NG); auto.
unfold eg in |- *.
apply shift_div_leEq.
apply pos_max_one.
Expand All @@ -932,7 +932,7 @@ Proof.
apply AbsIR_nonneg.
eapply shift_mult_leEq'.
apply pos_max_one.
unfold ef in HNF; unfold incf in |- *; apply HNF; apply le_trans with (max NF NG); auto.
unfold ef in HNF; unfold incf in |- *; apply HNF; apply Nat.le_trans with (max NF NG); auto.
unfold ef in |- *.
apply div_resp_pos.
apply pos_max_one.
Expand Down
12 changes: 6 additions & 6 deletions ftc/FunctSeries.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -608,7 +608,7 @@ Proof.
Transparent Frestr.
eapply leEq_wdr.
apply triangle_SumIR.
rewrite <- (S_pred m k); auto; apply lt_le_trans with N; auto.
rewrite <- (S_pred m k); auto; apply Nat.lt_le_trans with N; auto.
apply Sum_wd; intros.
Opaque FAbs.
simpl in |- *.
Expand All @@ -626,7 +626,7 @@ Proof.
apply Feq_imp_eq with I.
apply Feq_transitive with (FSum N (pred m) f).
unfold I in |- *; apply fun_seq_part_sum_n; auto with arith.
apply le_lt_trans with k; [ idtac | apply lt_le_trans with N ]; auto with arith.
apply Nat.le_lt_trans with k; [ idtac | apply Nat.lt_le_trans with N ]; auto with arith.
apply eq_imp_Feq.
unfold I in |- *; apply contin_imp_inc; Contin.
simpl in |- *.
Expand All @@ -641,15 +641,15 @@ Proof.
cut (Dom (FSum N (pred m) g) x). intro H6.
apply leEq_wdr with (Part _ _ H6).
apply FSum_resp_leEq.
rewrite <- (S_pred m k); auto; apply lt_le_trans with N; auto.
rewrite <- (S_pred m k); auto; apply Nat.lt_le_trans with N; auto.
intros.
Opaque FAbs.
simpl in |- *.
eapply leEq_wdl.
2: apply eq_symmetric_unfolded;
apply FAbs_char with (Hx' := contin_imp_inc _ _ _ _ (contF i) x0 (HxF i)).
apply Hk.
apply le_trans with N; auto with arith.
apply Nat.le_trans with N; auto with arith.
simpl in HxF.
apply (HxF 0).
cut (Dom (fun_seq_part_sum g m{-}fun_seq_part_sum g N) x). intro H7.
Expand All @@ -658,7 +658,7 @@ Proof.
simpl in |- *; rational.
apply Feq_imp_eq with I.
unfold I in |- *; apply fun_seq_part_sum_n; auto with arith.
apply le_lt_trans with k; [ idtac | apply lt_le_trans with N ]; auto with arith.
apply Nat.le_lt_trans with k; [ idtac | apply Nat.lt_le_trans with N ]; auto with arith.
auto.
split; simpl in |- *.
apply (contin_imp_inc _ _ _ _ (fun_seq_part_sum_cont _ _ _ _ contG m)); auto.
Expand All @@ -680,7 +680,7 @@ Proof.
auto with arith.
intros m H5 x H6 Hx Hx'.
apply AbsIR_imp_AbsSmall.
cut (N <= m); [ intro | apply le_trans with (max N k); auto with arith ].
cut (N <= m); [ intro | apply Nat.le_trans with (max N k); auto with arith ].
eapply leEq_wdl.
Transparent fun_seq_part_sum.
simpl in Hx'.
Expand Down
Loading