proposition: Theorem divP_invTerm_l : forall a b : Term A n, divP a b -> divP (invTerm (A:=A) invA (n:=n) a) b.
proof: Proof. Proof using plusA minusA cs A1. intros a b H'; inversion H'; auto. apply divTerm_def with (nZb := nZb); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (divTerm a nZb)) b); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (divTerm a nZb) b)); 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_l; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)