proposition: Lemma G_pres_plus : forall (IR : CReals) (x y : IR), (Build_CauchySeq Q_as_COrdField (fun m : nat => G IR (x[+]y) m) (CS_seq_G IR (x[+]y)) :R_COrdField Q_as_COrdField)[=] Build_CauchySeq Q_as_COrdField (fun m : nat => G IR x m[+]G IR y m) (CS_seq_plus Q_as_COrdField (fun n : nat => G IR x n) (fun n : nat => G IR y n) (CS_seq_G IR x) (CS_seq_G IR y)).
proof: Proof. intros. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := Build_CauchySeq Q_as_COrdField (fun m : nat => G IR (x[+]y) m) (CS_seq_G IR (x[+]y))) (y := Build_CauchySeq Q_as_COrdField (fun m : nat => G IR x m[+]G IR y m) (CS_seq_plus Q_as_COrdField (fun n : nat => G IR x n) (fun n : nat => G IR y n) (CS_seq_G IR x) ( CS_seq_G IR y))). intros e H. unfold CS_seq at 1 in |- *. unfold CS_seq in |- *. cut (SeqLimit (inj_Q_G_as_CauchySeq IR x) x). intro H0. cut (SeqLimit (inj_Q_G_as_CauchySeq IR y) y). intro H1. red in H0. cut {N : nat | forall m : nat, N <= m -> AbsSmall (inj_Q IR (e [/]ThreeNZ)) (CS_seq IR (inj_Q_G_as_CauchySeq IR x) m[-]x)}. intro H2. case H2. intro N1. intros. red in H1. cut {N : nat | forall m : nat, N <= m -> AbsSmall (inj_Q IR (e [/]ThreeNZ)) (CS_seq IR (inj_Q_G_as_CauchySeq IR y) m[-]y)}. intro H4. case H4. intro N2. intro H5. cut (SeqLimit (inj_Q_G_as_CauchySeq IR (x[+]y)) (x[+]y)). intro H6. red in H6. cut {N : nat | forall m : nat, N <= m -> AbsSmall (inj_Q IR (e [/]ThreeNZ)) (CS_seq IR (inj_Q_G_as_CauchySeq IR (x[+]y)) m[-](x[+]y))}. intro H7. case H7. intro K. intro H8. exists (K + (N1 + N2)). intros. apply AbsSmall_inj_Q with (R1 := IR). apply AbsSmall_wdr_unfolded with (y := inj_Q IR (G IR (x[+]y) m)[-] (inj_Q _ (G IR x m)[+]inj_Q _ (G IR y m))). rstepr (inj_Q _ (G IR (x[+]y) m)[-](x[+]y)[+](x[-]inj_Q _ (G IR x m))[+] (y[-]inj_Q _ (G IR y m))). apply AbsSmall_wdl_unfolded with (x := inj_Q IR (e [/]ThreeNZ)[+]inj_Q IR (e [/]ThreeNZ)[+] inj_Q IR (e [/]ThreeNZ)). apply AbsSmall_plus. apply AbsSmall_plus. change (AbsSmall (inj_Q IR (e [/]ThreeNZ)) (CS_seq IR (inj_Q_G_as_CauchySeq IR (x[+]y)) m[-](x[+]y))) in |- *. apply H8. apply Nat.le_trans with (m := K + (N1 + N2)). apply Nat.le_add_r. assumption. apply AbsSmall_minus. change (AbsSmall (inj_Q IR (e [/]ThreeNZ)) (CS_seq IR (inj_Q_G_as_CauchySeq IR x) m[-]x)) in |- *. apply a. apply Nat.le_trans with (m := K + (N1 + N2)). rewrite -> Nat.add_shuffle3 with (m := N1). apply Nat.le_add_r. assumption. apply AbsSmall_minus. change (AbsSmall (inj_Q IR (e [/]ThreeNZ)) (CS_seq IR (inj_Q_G_as_CauchySeq IR y) m[-]y)) in |- *. apply H5. apply Nat.le_trans with (m := K + (N1 + N2)). rewrite -> Nat.add_comm with (m := N2). rewrite -> Nat.add_shuffle3 with (m := N2). apply Nat.le_add_r. assumption. apply eq_transitive_unfolded with (y := inj_Q IR (e [/]ThreeNZ[+]e [/]ThreeNZ[+]e [/]ThreeNZ)). apply eq_transitive_unfolded with (y := inj_Q _ (e [/]ThreeNZ[+]e [/]ThreeNZ)[+]inj_Q IR (e [/]ThreeNZ)). apply bin_op_wd_unfolded. apply eq_symmetric_unfolded. apply inj_Q_plus. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply inj_Q_plus. apply inj_Q_wd. rational. apply eq_transitive_unfolded with (y := inj_Q IR (G IR (x[+]y) m)[-]inj_Q IR (G IR x m[+]G IR y m)). apply cg_minus_wd. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply inj_Q_plus. apply eq_symmetric_unfolded. apply inj_Q_minus. apply H6. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. apply div_resp_pos. apply pos_three. assumption. simpl in |- *. rational. apply x_is_SeqLimit_G. apply H1. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. apply div_resp_pos. apply pos_three. assumption. simpl in |- *. rational. apply H0. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. apply div_resp_pos. apply pos_three. assumption. simpl in |- *. rational. apply x_is_SeqLimit_G. apply x_is_SeqLimit_G. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism