proposition: Theorem f12_pres_plus : fun_pres_bin_fun R1 R2 f12 (csg_op (c:=R1)) (csg_op (c:=R2)).
proof: Proof. red in |- *. intros. unfold f12 in |- *. apply eq_transitive_unfolded with (y := Lim ((image_G_as_CauchySeq12 x:R_COrdField R2)[+] image_G_as_CauchySeq12 y)). apply Lim_well_def. unfold image_G_as_CauchySeq12 in |- *. apply eq_transitive_unfolded with (S := R_COrdField R2:CSetoid) (y := Build_CauchySeq R2 (fun m : nat => inj_Q R2 (G R1 x m[+]G R1 y m)) (inj_Q_Cauchy R2 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[+]G R1 y m) (CS_seq_plus Q_as_COrdField (fun n : nat => G R1 x n) (fun n : nat => G R1 y n) (CS_seq_G R1 x) (CS_seq_G R1 y)))) :R_COrdField R2). change ((Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 (x[+]y)) n)) (inj_Q_Cauchy R2 (G_as_CauchySeq R1 (x[+]y))) :R_COrdField R2)[=] Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[+]G R1 y m) (CS_seq_plus Q_as_COrdField (fun n : nat => G R1 x n) (fun n : nat => G R1 y n) (CS_seq_G R1 x) ( CS_seq_G R1 y))) m)) (inj_Q_Cauchy R2 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[+]G R1 y m) (CS_seq_plus Q_as_COrdField (fun n : nat => G R1 x n) (fun n : nat => G R1 y n) (CS_seq_G R1 x) ( CS_seq_G R1 y))))) in |- *. apply inj_seq_well_def. unfold G_as_CauchySeq in |- *. apply G_pres_plus. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := Build_CauchySeq R2 (fun m : nat => inj_Q R2 (G R1 x m[+]G R1 y m)) (inj_Q_Cauchy R2 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R1 x m[+]G R1 y m) (CS_seq_plus Q_as_COrdField (fun n : nat => G R1 x n) (fun n : nat => G R1 y n) (CS_seq_G R1 x) (CS_seq_G R1 y)))) :R_COrdField R2) (y := Build_CauchySeq R2 (fun m : nat => inj_Q R2 (G R1 x m)[+]inj_Q R2 (G R1 y m)) (CS_seq_plus R2 (fun n : nat => inj_Q R2 (G R1 x n)) (fun n : nat => inj_Q R2 (G R1 y n)) ( image_Cauchy12 x) (image_Cauchy12 y)) :R_COrdField R2). intros. exists 0. intros. unfold CS_seq in |- *. apply AbsSmall_wdr_unfolded with (y := [0]:R2). split. rstepr ([--]([0]:R2)). apply inv_resp_leEq. apply less_leEq. assumption. apply less_leEq. assumption. apply cg_cancel_rht with (x := inj_Q R2 (G R1 x m)[+]inj_Q R2 (G R1 y m)). astepl (inj_Q R2 (G R1 x m)[+]inj_Q R2 (G R1 y m)). apply eq_transitive_unfolded with (y := inj_Q R2 (G R1 x m[+]G R1 y m)). apply eq_symmetric_unfolded. apply inj_Q_plus. apply cg_cancel_mixed. apply Lim_pres_plus. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism