proposition: Theorem zeroP_multTerm_r : forall a b : Term, zeroP a -> zeroP (multTerm b a).
proof: Proof. Proof using plusA minusA invA divA cs A1. intros a b; case a; case b; simpl in |- *; auto. intros a1 H' b2 H'0 H'1; apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA a1 A0); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA A0 a1); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)