proposition: Lemma Q_dense_in_CReals : forall e : R1, [0] [<] e -> {q : Q_as_COrdField | [0] [<] inj_Q q | inj_Q q [<] e}.
proof: Proof. intros e H. cut {n : nat | ([1][/] e[//]Greater_imp_ap _ e [0] H) [<] nring (R:=R1) n}. intro H0. case H0. intro N. intros. exists (Qmake 1 (P_of_succ_nat N)). simpl in |- *. unfold pring in |- *; simpl in |- *. apply mult_cancel_less with (z := nring (R:=R1) N[+][1]). change ([0] [<] nring (R:=R1) (S N)) in |- *. apply pos_nring_S. astepl ([0]:R1). astepr (([0][+][1][-][0][/] nring (P_of_succ_nat N)[//] den_is_nonzero (Qmake 1%positive (P_of_succ_nat N)))[*] nring (S N)). rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ with N. rstepr ([1]:R1). apply pos_one. apply bin_op_wd_unfolded. rational. algebra. simpl in |- *. apply swap_div with (z_ := Greater_imp_ap _ e [0] H). rewrite nat_of_P_o_P_of_succ_nat_eq_succ. apply pos_nring_S. assumption. unfold pring in |- *; simpl in |- *. rstepl ([1][/] e[//]Greater_imp_ap _ e [0] H). apply less_transitive_unfolded with (y := nring (R:=R1) N). assumption. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. apply nring_less_succ. 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