proposition: Lemma mult_op_contin : forall f g h : CSetoid_un_op IR, contin f -> contin g -> (forall x, f x[*]g x [=] h x) -> contin h.
proof: Proof. intros f g h f_contin g_contin f_g_h. unfold contin in f_contin. unfold continAt in f_contin. unfold funLim in f_contin. unfold contin in g_contin. unfold continAt in g_contin. unfold funLim in g_contin. unfold contin in |- *. unfold continAt in |- *. unfold funLim in |- *. intros x e H. elim (mult_contin _ (f x) (g x) e H). intro b. intros H0 H1. elim H1. clear H1. intro c. intros H1 H2. elim (f_contin x b H0). clear f_contin. intro d'. intros H3 H4. elim (g_contin x c H1). clear g_contin. intro d''. intros H5 H6. exists (Min d' d''). apply less_Min; auto. intro x'. intros. astepr (f x[*]g x[-]f x'[*]g x'). apply H2. apply H4. apply AbsSmall_leEq_trans with (Min d' d''); auto. apply Min_leEq_lft. apply H6. apply AbsSmall_leEq_trans with (Min d' d''); auto. apply Min_leEq_rht. Qed.
imports: CoRN.reals.RealFuncts