proposition: Theorem divP_invTerm_r : forall a b : Term A n, divP a b -> divP a (invTerm (A:=A) invA (n:=n) b).
proof: Proof. Proof using plusA minusA cs A1. intros a b H'; inversion H'. cut (~ zeroP (A:=A) A0 eqA (n:=n) (invTerm (A:=A) invA (n:=n) b)); [ intros nZib | auto ]. apply divTerm_def with (nZb := nZib); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (divTerm a nZb)) (invTerm (A:=A) invA (n:=n) b)); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (divTerm a nZb) (invTerm (A:=A) invA (n:=n) b))); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (divTerm a nZb) b))); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm a nZb) b); auto. apply eqTerm_invTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply mult_invTerm_com_r with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply mult_invTerm_com with (1 := cs); auto. apply eqTerm_multTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply divTerm_invTerm_r; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)