proposition: Lemma cpoly_mult_op_strext : bin_op_strext cpoly_csetoid cpoly_mult_cs.
proof: Proof. do 4 intro. pattern x1, x2 in |- *. apply Ccpoly_double_ind0_cs. rewrite cpoly_zero_mult. intro; pattern p in |- *; apply Ccpoly_ind_cs. rewrite cpoly_zero_mult. auto. do 2 intro. rewrite cpoly_lin_mult. intros. cut ((c [#] [0] or p0 [#] cpoly_zero_cs) or y1 [#] y2). intro H1. elim H1. intro; left; apply _cpoly_lin_ap_zero; assumption. auto. cut (cpoly_plus_cs (cpoly_mult_cr_cs y1 c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 y1)) [#] cpoly_plus_cs (cpoly_mult_cr_cs y2 [0]) (cpoly_linear_cs [0] (cpoly_mult_cs cpoly_zero_cs y2))). intro H1. elim (cpoly_plus_op_strext _ _ _ _ H1); intro H2. elim (cpoly_mult_cr_strext _ _ _ _ H2); auto. elim H2; intro H3. elim (ap_irreflexive _ _ H3). rewrite cpoly_zero_mult in H3. elim X; auto. rewrite cpoly_zero_mult. apply ap_wdr_unfolded with cpoly_zero_cs. assumption. astepl (cpoly_plus_cs cpoly_zero_cs cpoly_zero_cs). apply cpoly_plus_op_wd. apply eq_symmetric_unfolded. apply cpoly_mult_cr_zero. apply _cpoly_zero_eq_lin. split; algebra. intro; pattern p in |- *; apply Ccpoly_ind_cs. auto. intros. cut ((c [#] [0] or cpoly_zero_cs [#] p0) or y1 [#] y2). intro. elim X1; try auto. cut (cpoly_plus_cs (cpoly_mult_cr_cs y1 [0]) (cpoly_linear_cs [0] (cpoly_mult_cs cpoly_zero_cs y1)) [#] cpoly_plus_cs (cpoly_mult_cr_cs y2 c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 y2))). intro H1. elim (cpoly_plus_op_strext _ _ _ _ H1); intro H2. elim (cpoly_mult_cr_strext _ _ _ _ H2); auto. intro. left. left. apply ap_symmetric_unfolded. assumption. cut (([0]:CR) [#] [0] or cpoly_mult_cs cpoly_zero_cs y1 [#] cpoly_mult_cs p0 y2). 2: apply cpoly_lin_ap_lin_; auto. clear H2; intro H2. elim H2; intro H3. elim (ap_irreflexive _ _ H3). rewrite cpoly_zero_mult in H3. elim X; auto. rewrite cpoly_zero_mult. apply ap_wdl_unfolded with cpoly_zero_cs. assumption. astepl (cpoly_plus_cs cpoly_zero_cs cpoly_zero_cs). apply cpoly_plus_op_wd. apply eq_symmetric_unfolded. apply cpoly_mult_cr_zero. apply _cpoly_zero_eq_lin. split; algebra. intros. cut ((c [#] d or p [#] q) or y1 [#] y2). intro. auto. elim (cpoly_plus_op_strext _ _ _ _ X0); intro H1. elim (cpoly_mult_cr_strext _ _ _ _ H1); auto. elim H1; intro H2. elim (ap_irreflexive _ _ H2). elim X; auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational