proposition: Theorem divTerm_invTerm_r : forall (a b : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a) (nZia : ~ zeroP (A:=A) A0 eqA (n:=n) (invTerm (A:=A) invA (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 b nZia) (invTerm (A:=A) invA (n:=n) (divTerm b nZa)).
proof: Proof. Proof using plusA minusA cs A1. intros a b; case a; case b; simpl in |- *; auto. split; auto. apply divA_invA_r with (1 := cs); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)