proposition: Lemma image_Cauchy12 : forall x : R1, Cauchy_prop (fun n : nat => inj_Q R2 (G R1 x n)).
proof: Proof. intros. change (Cauchy_prop (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 x) n))) in |- *. apply inj_Q_Cauchy. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism