proposition: Theorem divP_multTerm_l : forall a b c : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> eqTerm (A:=A) eqA (n:=n) (multTerm (A:=A) multA (n:=n) a b) c -> divP c a.
proof: Proof. Proof using plusA minusA invA eqA_dec cs A1. intros a b c H' H'0 H'1. apply divP_comp with (a := multTerm (A:=A) multA (n:=n) a b) (c := a); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)