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