proposition: Lemma Cauchy_Lim_mult : forall seq1 seq2 y1 y2, Cauchy_Lim_prop2 seq1 y1 -> Cauchy_Lim_prop2 seq2 y2 -> Cauchy_Lim_prop2 (fun n => seq1 n [*] seq2 n) (y1 [*] y2).
proof: Proof. unfold Cauchy_Lim_prop2 in |- *. intros. rename X into H. rename X0 into H0. rename X1 into H1. elim (mult_contin _ y1 y2 eps H1). intro c. intros H2 H3. elim H3. clear H3. intro d. intros H3 H4. elim (H c H2). clear H. intro N1. intros H. elim (H0 d H3). clear H0. intro N2. intros H0. cut {N : nat | N1 <= N /\ N2 <= N}. intro H5. elim H5. clear H5. intro N. intro H5. elim H5. clear H5. intros. exists N. intros. apply AbsSmall_wdr_unfolded with ([--] (y1[*]y2[-]seq1 m[*]seq2 m)). apply inv_resp_AbsSmall. apply H4; clear H4; intros. apply AbsSmall_wdr_unfolded with ([--] (seq1 m[-]y1)). apply inv_resp_AbsSmall. apply H. apply Nat.le_trans with N; auto. rational. apply AbsSmall_wdr_unfolded with ([--] (seq2 m[-]y2)). apply inv_resp_AbsSmall. apply H0. apply Nat.le_trans with N; auto. rational. rational. elim (le_lt_dec N1 N2); intros. exists N2. auto. exists N1. split. auto. auto with arith. Qed.
imports: CoRN.reals.CReals Coq(Lia)