proposition: Lemma cpoly_mult_cr_strext : bin_fun_strext _ _ _ cpoly_mult_cr_cs.
proof: Proof. unfold bin_fun_strext in |- *. do 4 intro. pattern x1, x2 in |- *. apply Ccpoly_double_ind0_cs. intro. rewrite cpoly_zero_mult_cr. intro H. left. generalize H. pattern p in |- *. apply Ccpoly_ind_cs. rewrite cpoly_zero_mult_cr. auto. do 2 intro. rewrite cpoly_lin_mult_cr. intros. cut (y1[*]c [#] [0] or cpoly_mult_cr_cs p0 y1 [#] cpoly_zero_cs). 2: apply cpoly_lin_ap_zero_. 2: auto. clear H0; intro H1. cut (c [#] [0] or p0 [#] cpoly_zero_cs). intro; apply _cpoly_lin_ap_zero. auto. elim H1; intro H2. generalize (cring_mult_ap_zero_op _ _ _ H2); intro. auto. right. auto. rewrite cpoly_zero_mult_cr. intros. left. generalize X. pattern p in |- *; apply Ccpoly_ind_cs. rewrite cpoly_zero_mult_cr. auto. do 2 intro. rewrite cpoly_lin_mult_cr. intros. cut (y2[*]c [#] [0] or cpoly_zero_cs [#] cpoly_mult_cr_cs p0 y2). 2: apply cpoly_zero_ap_lin_. 2: auto. clear X1; intro H1. cut (c [#] [0] or cpoly_zero_cs [#] p0). intro. apply _cpoly_zero_ap_lin. auto. elim H1; intro H2. generalize (cring_mult_ap_zero_op _ _ _ H2); auto. right. auto. do 4 intro. repeat rewrite cpoly_lin_mult_cr. intros. cut (y1[*]c [#] y2[*]d or cpoly_mult_cr_cs p y1 [#] cpoly_mult_cr_cs q y2). 2: apply cpoly_lin_ap_lin_. 2: auto. clear X0; intro H0. cut ((c [#] d or p [#] q) or y1 [#] y2). intro. elim X0; try auto. elim H0; intro H1. generalize (cs_bin_op_strext _ _ _ _ _ _ H1); tauto. elim X; auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational