proposition: Lemma Q_dense_in_CReals' : forall a b : R1, a [<] b -> {q : Q_as_COrdField | a [<] inj_Q q | inj_Q q [<] b}.
proof: Proof. cut (forall a b : R1, [0][<]b -> a[<]b -> {q : Q_as_COrdField | a[<]inj_Q q | inj_Q q[<]b}). intros H a b Hab. destruct (less_cotransitive_unfolded _ _ _ Hab [0]);[|apply H;assumption]. assert (X:[0][<][--]a). rstepl ([--][0]:R1). apply inv_resp_less. assumption. assert (Y:=inv_resp_less _ _ _ Hab). destruct (H _ _ X Y) as [q Hqa Hqb]. exists (-q)%Q. stepr ([--](inj_Q q)). apply inv_cancel_less. stepl (inj_Q q);[assumption|apply eq_symmetric; apply cg_inv_inv]. apply eq_symmetric; apply inj_Q_inv. stepl ([--](inj_Q q)). apply inv_cancel_less. stepr (inj_Q q);[assumption|apply eq_symmetric; apply cg_inv_inv]. apply eq_symmetric; apply inj_Q_inv. cut (forall a b : R1, [0][<]b -> (a[+][1])[<]b -> {n : nat | a[<]nring n | nring n[<]b}). intros H a b Hb Hab. destruct (Q_dense_in_CReals _ (shift_zero_less_minus _ _ _ Hab)) as [q Haq Hbq]. assert (X0 := pos_ap_zero _ _ Haq). assert (X1 : [0][<](b[/]inj_Q q[//]X0)). apply div_resp_pos; assumption. assert (X2 : (a[/]inj_Q q[//]X0)[+][1][<](b[/]inj_Q q[//]X0)). apply shift_plus_less'. rstepr ((b[-]a)[/]inj_Q q[//]X0). apply shift_less_div. assumption. rstepl (inj_Q q). assumption. destruct (H _ _ X1 X2) as [r Hra Hrb]. exists ((nring r)[*]q)%Q; csetoid_rewrite (inj_Q_mult (nring r) q). eapply shift_less_mult. assumption. stepr (nring (R:=R1) r). apply Hra. apply eq_symmetric. apply inj_Q_nring. eapply shift_mult_less. assumption. stepl (nring (R:=R1) r). apply Hrb. apply eq_symmetric. apply inj_Q_nring. intros a b Hb Hab. destruct (Archimedes' a) as [n Hn]. induction n. exists 0; try assumption. destruct (less_cotransitive_unfolded _ _ _ Hab (nring (R:=R1) (S n))). apply IHn. apply plus_cancel_less with [1]. apply c. exists (S n); assumption. 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