proposition: Theorem zeroP_invTerm_zeroP : forall a : Term, zeroP a -> zeroP (invTerm a).
proof: Proof. Proof using plusA multA minusA divA cs A1. intros a; case a; simpl in |- *; auto. intros b H' H'0; apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := plusA A0 (invA A0)); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := invA A0); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := plusA (invA A0) A0); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)