proposition: Lemma Lim_pres_mult : forall (IR : CReals) (g h : R_COrdField IR), Lim (g[*]h)[=]Lim g[*]Lim h.
proof: Proof. intros. apply eq_symmetric_unfolded. apply SeqLimit_unique with (g := g[*]h). red in |- *. simpl in |- *. intros. case (CS_seq_bounded IR (CS_seq IR g) (CS_proof IR g)). intro K. set (H2 := True) in *. intros H3 H4. case H4. intro M1. intro H5. case (nonarchemaedian_bound_for_Lim _ h). intro L. set (H6 := True) in *. intros H7 H8. cut (Six[*]K[#][0]). intro H9. cut (Six[*]L[#][0]). intro H10. case (ax_Lim _ _ (crl_proof IR) g (e[/] Six[*]L[//]H10)). apply div_resp_pos. apply mult_resp_pos. apply pos_nring_S. assumption. assumption. intro N1. intro H11. case (ax_Lim _ _ (crl_proof IR) h (e[/] Six[*]K[//]H9)). apply div_resp_pos. apply mult_resp_pos. apply pos_nring_S. apply leEq_not_eq. apply (AbsSmall_nonneg IR K (CS_seq IR g M1)). apply H5. constructor. apply less_imp_ap; auto. assumption. intro N2. intro H12. exists (N1 + (N2 + M1)). intros m H13. rstepr (CS_seq IR g m[*](CS_seq IR h m[-]Lim h)[+]Lim h[*](CS_seq IR g m[-]Lim g)). rstepl (Three[*](K[*](e[/] Six[*]K[//]H9))[+]Three[*](L[*](e[/] Six[*]L[//]H10))). apply AbsSmall_plus. apply AbsSmall_mult. apply H5. apply Nat.le_trans with (m := N1 + (N2 + M1)). rewrite -> Nat.add_comm with (m := M1). rewrite -> Nat.add_shuffle3 with (m := M1). apply Nat.le_add_r. assumption. apply H12. apply Nat.le_trans with (m := N1 + (N2 + M1)). rewrite -> Nat.add_shuffle3 with (m := N2). apply Nat.le_add_r. assumption. apply AbsSmall_mult. assumption. apply H11. apply Nat.le_trans with (m := N1 + (N2 + M1)). apply Nat.le_add_r. assumption. apply Greater_imp_ap. apply mult_resp_pos. apply pos_nring_S. assumption. apply Greater_imp_ap. apply mult_resp_pos. apply pos_nring_S. apply leEq_not_eq. apply (AbsSmall_nonneg IR K (CS_seq IR g M1)). apply H5. constructor. apply less_imp_ap; auto. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism