proposition: Lemma CS_seq_inj_Q_G : forall x : R1, Cauchy_prop (fun m : nat => inj_Q R1 (G x m)).
proof: Proof. intro. change (Cauchy_prop (fun m : nat => inj_Q R1 (CS_seq _ (G_as_CauchySeq x) m))) in |- *. apply inj_Q_Cauchy. Qed.
imports: CoRN.reals.Q_in_CReals