proposition: Lemma invTerm_T1_eqT_comp : forall a b : Term A n, eqT a b -> eqT a (invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) b)).
proof: Proof. Proof using plusA minusA eqA divA cs A0. intros a b H'. apply (eqT_trans A n) with (y := b); auto. apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) b); auto. apply (T1_eqT A A1 eqA); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)