proposition: Lemma Cauchy_IR_mult_as_CR_mult : forall x y:Cauchy_IR, ((Cauchy_IRasCR x)*(Cauchy_IRasCR y) == Cauchy_IRasCR (x[*]y))%CR.
proof: Proof. intros x [y Hy]. destruct (CS_seq_bounded _ y Hy) as [k Hk [n Hn]]. set (y':=Build_CauchySeq Q_as_COrdField y Hy). set (k':=(exist _ _ Hk)). transitivity ((ucFun2 (CRmult_bounded (CR_b (1 # 1) (Cauchy_IRasCR y')+k')%Qpos) (Cauchy_IRasCR x) (Cauchy_IRasCR y'))). apply CRmult_bounded_weaken. apply CR_b_lowerBound. apply CR_b_upperBound. simpl. rewrite -> Qle_minus_iff. ring_simplify. auto with *. apply Cauchy_IR_mult_as_CRmult_bounded with n. intros i Hi. eapply AbsSmall_trans;[|apply Hn;assumption]. simpl. rewrite -> Qlt_minus_iff. unfold k'. autorewrite with QposElim. ring_simplify. clear. destruct Hy. rewrite Qplus_comm. apply Q.Qplus_lt_le_0_compat. reflexivity. apply Qabs_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps