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