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