proposition: Theorem divTerm_multTerm_l : forall (a b c : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), eqTerm (A:=A) eqA (n:=n) b (multTerm (A:=A) multA (n:=n) (divTerm b nZa) a) -> eqTerm (A:=A) eqA (n:=n) (divTerm (multTerm (A:=A) multA (n:=n) c b) nZa) (multTerm (A:=A) multA (n:=n) c (divTerm b nZa)).
proof: Proof. Proof using plusA minusA invA cs A1. intros a b c; case a; case b; case c; simpl in |- *; auto. intros d c0 A0' c2 d2 c3 nZd2 H'0; case H'0; intros H'1 H'2; auto. split; auto. apply divA_multA_comp_l with (1 := cs). rewrite H'2. repeat rewrite mult_div_com. rewrite mult_mon_assoc. repeat rewrite mult_div_com; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)