proposition: Theorem g21_pres_mult : fun_pres_bin_fun R2 R1 g21 (cr_mult (c:=R2)) (cr_mult (c:=R1)).
proof: Proof. red in |- *. intros. unfold g21 in |- *. apply eq_transitive_unfolded with (y := Lim ((image_G_as_CauchySeq21 x:R_COrdField R1)[*] image_G_as_CauchySeq21 y)). apply Lim_well_def. unfold image_G_as_CauchySeq21 in |- *. apply eq_transitive_unfolded with (S := R_COrdField R1:CSetoid) (y := Build_CauchySeq R1 (fun m : nat => inj_Q R1 (G R2 x m[*]G R2 y m)) (inj_Q_Cauchy R1 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R2 x m[*]G R2 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R2 x)) (CS_proof _ (G_as_CauchySeq R2 y))))) :R_COrdField R1). change ((Build_CauchySeq R1 (fun n : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 (x[*]y)) n)) (inj_Q_Cauchy R1 (G_as_CauchySeq R2 (x[*]y))) :R_COrdField R1)[=] Build_CauchySeq R1 (fun m : nat => inj_Q R1 (CS_seq Q_as_COrdField (Build_CauchySeq Q_as_COrdField (fun m : nat => G R2 x m[*]G R2 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R2 x)) (CS_proof _ (G_as_CauchySeq R2 y)))) m)) (inj_Q_Cauchy R1 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R2 x m[*]G R2 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R2 x)) (CS_proof _ (G_as_CauchySeq R2 y)))))) in |- *. apply inj_seq_well_def. unfold G_as_CauchySeq in |- *. change ((Build_CauchySeq Q_as_COrdField (fun m : nat => G R2 (x[*]y) m) (CS_seq_G R2 (x[*]y)) :R_COrdField Q_as_COrdField)[=] Build_CauchySeq Q_as_COrdField (fun m : nat => G R2 x m[*]G R2 y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq R2 x)) (CS_proof _ (G_as_CauchySeq R2 y)))) in |- *. apply G_pres_mult. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := Build_CauchySeq R1 (fun m : nat => inj_Q R1 (G R2 x m[*]G R2 y m)) (inj_Q_Cauchy R1 (Build_CauchySeq Q_as_COrdField (fun m : nat => G R2 x m[*]G R2 y m) (CS_seq_mult Q_as_COrdField (G_as_CauchySeq R2 x) (G_as_CauchySeq R2 y) (CS_proof Q_as_COrdField (G_as_CauchySeq R2 x)) (CS_proof Q_as_COrdField (G_as_CauchySeq R2 y)))))) (y := Build_CauchySeq R1 (fun m : nat => inj_Q R1 (G R2 x m)[*]inj_Q R1 (G R2 y m)) (CS_seq_mult R1 (image_G_as_CauchySeq21 x) (image_G_as_CauchySeq21 y) (CS_proof R1 (image_G_as_CauchySeq21 x)) (CS_proof R1 (image_G_as_CauchySeq21 y)))). intros. exists 0. intros. unfold CS_seq in |- *. apply AbsSmall_wdr_unfolded with (y := [0]:R1). split. rstepr ([--]([0]:R1)). apply inv_resp_leEq. apply less_leEq. assumption. apply less_leEq. assumption. apply cg_cancel_rht with (x := inj_Q R1 (G R2 x m)[*]inj_Q R1 (G R2 y m)). astepl (inj_Q R1 (G R2 x m)[*]inj_Q R1 (G R2 y m)). apply eq_transitive_unfolded with (y := inj_Q R1 (G R2 x m[*]G R2 y m)). apply eq_symmetric_unfolded. apply inj_Q_mult. apply cg_cancel_mixed. apply Lim_pres_mult. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism