proposition: Theorem multTerm_minusTerm_dist_l : forall a b c : Term, eqT a b -> eqTerm (minusTerm (multTerm a c) (multTerm b c)) (multTerm (minusTerm a b) c).
proof: Proof. Proof using plusA invA divA cs A1 A0. intros a b c eqT1. apply eqTerm_trans with (y := multTerm (plusTerm a (invTerm b)) c); auto. apply eqTerm_trans with (y := plusTerm (multTerm a c) (multTerm (invTerm b) c)); auto. apply eqTerm_trans with (y := plusTerm (multTerm a c) (invTerm (multTerm b c))); auto. apply eqTerm_minusTerm_plusTerm_invTerm; auto. apply eqTerm_plusTerm_comp; auto. apply eqT_trans with (y := multTerm b c); auto. apply multTerm_eqT; auto. apply invTerm_eqT; auto. apply multTerm_eqT; auto. apply eqT_trans with (y := b); auto. apply invTerm_eqT; auto. apply eqTerm_refl; auto. apply eqTerm_sym; apply mult_invTerm_com; auto. apply multTerm_plusTerm_dist_l; auto. apply eqTerm_multTerm_comp; auto. apply eqTerm_sym; apply eqTerm_minusTerm_plusTerm_invTerm; auto. apply eqTerm_refl; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)