proposition: Theorem multTerm_plusTerm_dist_l : forall a b c : Term, eqTerm (plusTerm (multTerm a c) (multTerm b c)) (multTerm (plusTerm a b) c).
proof: Proof. Proof using minusA invA divA cs A1 A0. intros a b c; case a; case b; case c; simpl in |- *; auto. intros a1 m1 a2 m2 a3 m3; split; auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (plusA (multA a1 a3) (multA a1 a2)); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (multA a1 (plusA a3 a2)); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)