proposition: Theorem invTerm_T1_multTerm_T1 : eqTerm (A:=A) eqA (n:=n) (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (invTerm (A:=A) invA (n:=n) (T1 A1 n))) (T1 A1 n).
proof: Proof. Proof using plusA minusA divA cs A0. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)))); [ auto | idtac ]. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n))); auto. apply eqTerm_invTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply T1_multTerm_l with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply invTerm_invol with (1 := cs); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)