proposition: Lemma cpoly_mult_fast_op_strext : bin_op_strext cpoly_csetoid cpoly_mult_fast_cs.
proof: Proof. intros x1 x2 y1 y2 H. apply cpoly_mult_op_strext. stepl (cpoly_mult_fast_cs x1 y1). stepr (cpoly_mult_fast_cs x2 y2). assumption. apply cpoly_mult_fast_equiv. apply cpoly_mult_fast_equiv. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational