proposition: Lemma cpoly_linear_strext : bin_fun_strext _ _ _ cpoly_linear_cs.
proof: Proof. unfold bin_fun_strext in |- *. intros until 1. apply cpoly_lin_ap_lin_;assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational