proposition: Theorem invTerm_invol : forall a : Term, eqTerm a (invTerm (invTerm a)).
proof: Proof. Proof using plusA multA minusA divA cs A1 A0. intros a; case a; simpl in |- *; auto. intros a0 m; split; auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA a0 A0); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA a0 (plusA (invA a0) (invA (invA a0)))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (plusA a0 (invA a0)) (invA (invA a0))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA A0 (invA (invA a0))); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (invA (invA a0)) A0); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)