proposition: Lemma cpoly_inv_op_strext : un_op_strext cpoly_csetoid cpoly_inv_cs.
proof: Proof. unfold un_op_strext in |- *. unfold fun_strext in |- *. intros x y. pattern x, y in |- *. apply Ccpoly_double_sym_ind0_cs. unfold Csymmetric in |- *. intros. apply ap_symmetric_unfolded. apply X. apply ap_symmetric_unfolded. assumption. intro p; pattern p in |- *; apply Ccpoly_ind_cs. auto. intros. cut ( [--]c [#] [0] or cpoly_inv_cs p0 [#] cpoly_zero_cs). 2: apply cpoly_lin_ap_zero_. 2: auto. clear X0; intro H0. apply _cpoly_lin_ap_zero. auto. elim H0. left. astepl ( [--][--]c). algebra. right. apply X. assumption. intros. cut ( [--]c [#] [--]d or cpoly_inv_cs p [#] cpoly_inv_cs q). 2: apply cpoly_lin_ap_lin_. 2: auto. clear X0; intro H0. auto. elim H0; intro. left. astepl ( [--][--]c). astepr ( [--][--]d). apply inv_resp_ap. assumption. right. apply X. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational