proposition: Theorem divTerm_multTerm_r : 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) b c) nZa) (multTerm (A:=A) multA (n:=n) (divTerm b nZa) c).
proof: Proof. Proof using plusA minusA invA cs A1. intros a b c; case a; case b; case c; simpl in |- *; auto. intros a0 m a1 m0 a2 m1 nZa H'; split; auto. apply divA_multA_comp_r with (1 := cs). elim H'; intros H'0 H'1; rewrite H'1; clear H'. rewrite mult_div_com; auto. rewrite <- mult_mon_assoc. rewrite (mult_mon_com n m1 m). rewrite mult_mon_assoc. rewrite mult_div_com; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)