proposition: Theorem mult_invTerm_com : forall a b : Term, eqTerm (multTerm (invTerm a) 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 (invA a1) a0) A0); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (multA (invA a1) a0) (plusA (multA a1 a0) (invA (multA a1 a0)))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (plusA (multA (invA a1) a0) (multA a1 a0)) (invA (multA a1 a0))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (multA (plusA (invA a1) a1) a0) (invA (multA a1 a0))); auto. apply plusA_eqA_comp with (1 := cs); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (multA a0 (invA a1)) (multA a0 a1)); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (multA a0 (plusA (invA a1) a1)); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (multA (plusA a1 (invA a1)) a0) (invA (multA a1 a0))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (multA A0 a0) (invA (multA a1 a0))); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); 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)