proposition: Lemma cpoly_cg_proof : is_CGroup cpoly_cmonoid cpoly_inv_op.
proof: Proof. intro x. unfold is_inverse in |- *. assert (x[+]cpoly_inv_cs x [=] [0]). pattern x in |- *; apply cpoly_ind_cs. rewrite cpoly_inv_zero. rewrite -> cpoly_plus_zero. simpl; auto. intros. rewrite cpoly_inv_lin. rewrite -> cpoly_lin_plus_lin. apply _cpoly_lin_eq_zero. split;[algebra|assumption]. split; auto. eapply eq_transitive_unfolded. apply cpoly_plus_commutative. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational