proposition: Theorem inj_Q_Cauchy : forall g : CauchySeq Q_as_COrdField, Cauchy_prop (fun n => inj_Q (g n)).
proof: Proof. intros. case g. intros g_ pg. simpl in |- *. red in |- *. intros e H. cut {n : nat | ([1][/]e[//]Greater_imp_ap _ e [0] H) [<] nring (R:=R1) n}. intro H0. case H0. intros N1 H1. unfold Cauchy_prop in pg. cut {N : nat | forall m : nat, N <= m -> AbsSmall (R:=Q_as_COrdField) (Qmake 1%Z (P_of_succ_nat N1)) (g_ m[-]g_ N)}. intro H2. case H2. intro N. intro. exists N. intros. apply AbsSmall_leEq_trans with (e1 := inj_Q (Qmake 1%Z (P_of_succ_nat N1))). apply less_leEq. apply mult_cancel_less with (z := nring (R:=R1) (S N1)[*]([1][/]e[//]Greater_imp_ap _ e [0] H)). apply mult_resp_pos. apply pos_nring_S. apply div_resp_pos. assumption. apply pos_one. unfold inj_Q in |- *. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ with N1. rstepl ([1][/]e[//]Greater_imp_ap _ e [0] H). rstepr (nring (R:=R1) (P_of_succ_nat N1)). apply less_transitive_unfolded with (y := nring (R:=R1) N1). assumption. apply nring_less. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. apply Nat.lt_succ_diag_r. astepr (inj_Q (g_ m[-]g_ N)). apply inj_Q_AbsSmall. apply a. assumption. apply pg. simpl in |- *. red in |- *. simpl in |- *. constructor. apply Archimedes'. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac