proposition: Theorem divP_comp_ppc0 : forall (a b : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a) (nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b) (nZppab : ~ zeroP (A:=A) A0 eqA (n:=n) (ppc a b)) (p : list (Term A n)), eqTerm (A:=A) eqA (n:=n) b (multTerm (A:=A) multA (n:=n) (divTerm (multTerm (A:=A) multA (n:=n) a b) nZppab) (divTerm (ppc a b) nZa)).
proof: Proof. Proof using plusA minusA invA eqA_dec cs. intros a b nZa nZb nZppab p. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm a nZa) b); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := divTerm (multTerm (A:=A) multA (n:=n) a b) nZa); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)