proposition: Lemma cpoly_plus_op_strext : bin_op_strext cpoly_csetoid cpoly_plus_cs.
proof: Proof. unfold bin_op_strext in |- *. unfold bin_fun_strext in |- *. intros x1 x2. pattern x1, x2 in |- *. apply Ccpoly_double_sym_ind0_cs. unfold Csymmetric in |- *. intros. generalize (ap_symmetric_unfolded _ _ _ X0); intro H1. generalize (X _ _ H1); intro H2. elim H2; intro H3; generalize (ap_symmetric_unfolded _ _ _ H3); auto. intro p; pattern p in |- *; apply Ccpoly_ind_cs. intro; intro H. simpl in |- *; auto. intros s c H y1 y2. pattern y1, y2 in |- *. apply Ccpoly_double_ind0_cs. intros p0 H0. apply cpoly_ap_zero_plus. apply H0. intro p0. intro H0. elim (ap_cotransitive _ _ _ H0 cpoly_zero_cs); auto. do 4 intro. intros. cut (c[+]c0 [#] d or cpoly_plus_cs s p0 [#] q). 2: apply cpoly_lin_ap_lin_; assumption. clear X0; intro H1. elim H1; intro H2. cut (c[+]c0 [#] [0][+]d). intro H3. elim (cs_bin_op_strext _ _ _ _ _ _ H3). intro H4. left. apply _cpoly_lin_ap_zero. auto. intro. right. apply _cpoly_lin_ap_lin. auto. astepr d. auto. elim (H _ _ H2); auto. intro. left. apply _cpoly_lin_ap_zero. auto. right. apply _cpoly_lin_ap_lin. auto. do 7 intro. pattern y1, y2 in |- *. apply Ccpoly_double_ind0_cs. intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs. auto. intros. cut (c[+]c0 [#] d or cpoly_plus_cs p p1 [#] q). intro H2. 2: apply cpoly_lin_ap_lin_. 2: auto. elim H2; intro H3. cut (c[+]c0 [#] d[+][0]). intro H4. elim (cs_bin_op_strext _ _ _ _ _ _ H4). intro. left. apply _cpoly_lin_ap_lin. auto. intro. right. apply _cpoly_lin_ap_zero. auto. astepr d. auto. elim X with p1 cpoly_zero_cs. intro. left. apply _cpoly_lin_ap_lin. auto. right. apply _cpoly_lin_ap_zero. auto. rewrite cpoly_plus_zero. assumption. intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs. auto. intros. cut (c [#] d[+]c0 or p [#] cpoly_plus_cs q p1). 2: apply cpoly_lin_ap_lin_. 2: assumption. clear X1; intro H1. elim H1; intro H2. cut (c[+][0] [#] d[+]c0). intro H3. elim (cs_bin_op_strext _ _ _ _ _ _ H3). intro. left. unfold cpoly_linear_cs in |- *; simpl in |- *; auto. intro. right. left. apply ap_symmetric_unfolded. assumption. astepl c. auto. elim X with cpoly_zero_cs p1. intro. left. unfold cpoly_linear_cs in |- *; simpl in |- *; auto. intro. right. right; auto. rewrite cpoly_plus_zero. assumption. intros. elim X1; intro H2. elim (cs_bin_op_strext _ _ _ _ _ _ H2); auto. intro. left. left; auto. intro. right. left; auto. simpl in H2. elim (X _ _ H2). intro. left; right; auto. right; right; auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational