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