proposition: Lemma cpoly_op_contin : forall g : cpoly IR, contin (cpoly_csetoid_op _ g).
proof: Proof. intro g. elim g. unfold contin in |- *. unfold continAt in |- *. unfold funLim in |- *. intros. exists OneR. apply pos_one. intros. simpl in |- *. unfold AbsSmall in |- *. split; apply less_leEq. rstepr ([--]ZeroR). apply inv_resp_less. auto. astepl ZeroR. auto. intros a f. intros. apply linear_op_contin with (cpoly_csetoid_op _ f) a. auto. intros. simpl in |- *. rational. Qed.
imports: CoRN.reals.RealFuncts