proposition: Lemma Q_dense_in_R : forall x, [0] [<] x -> {q : F | [0] [<] q | inject_Q q [<] x}.
proof: Proof. intros. cut (x [#] [0]). intro H0. cut {n : nat | ([1][/] x[//]H0) [<=] nring n}. intro H1. case H1. intros n H2. cut (nring (R:=F) (S n) [#] [0]). intro H3. exists ([1][/] nring (S n) [//]H3). apply recip_resp_pos. apply ing_cancel_less. change ([0] [<] inject_Q (nring (S n))) in |- *. apply less_leEq_trans with (R := R_COrdField') (y := [1][/] x[//]H0). apply recip_resp_pos. assumption. apply leEq_transitive with (inject_Q (nring n)). astepr (nring (R:=R_COrdField') n). assumption. apply ing_nring. astepl (nring (R:=R_COrdField') n). astepr (nring (R:=R_COrdField') (S n)). apply less_leEq; astepr (nring (R:=R_COrdField') n[+][1]); apply less_plusOne. apply ing_nring. apply ing_nring. cut (nring (R:=R_COrdField') (S n) [#] [0]). intro H4. astepl (inject_Q ([1]:F) [/] nring (S n) [//]H4). apply shift_div_less. apply nring_pos. auto with arith. astepl ([1]:R_COrdField'). apply shift_less_mult' with H0. assumption. eapply leEq_less_trans. apply H2. astepr (nring (R:=R_COrdField') n[+][1]); apply less_plusOne. apply ing_n. apply nringS_ap_zero. apply nringS_ap_zero. apply R_is_archemaedian. apply Greater_imp_ap. assumption. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals