Lemma plus_op_contin : forall f g h : CSetoid_un_op IR,
 contin f -> contin g -> (forall x, f x[+]g x [=] h x) -> contin h.









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.









Lemma linear_op_contin : forall (f g : CSetoid_un_op IR) a,
 contin f -> (forall x, x[*]f x[+]a [=] g x) -> contin g.











Lemma cpoly_op_contin : forall g : cpoly IR, contin (cpoly_csetoid_op _ g).