proposition: Theorem divTerm_multTermr : forall a b : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> divP (multTerm (A:=A) multA (n:=n) a b) b.
proof: Proof. Proof using plusA minusA invA eqA_dec cs A1. intros a b nZa nZb. apply divTerm_def with (nZb := nZb); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (multTerm (A:=A) multA (n:=n) a (divTerm b nZb)) b); auto. apply eqTerm_multTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply divTerm_multTerm_l; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)