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