proposition: Theorem minusTerm_zeroP : forall a b : Term A n, eqT a b -> zeroP (A:=A) A0 eqA (n:=n) b -> eqTerm (A:=A) eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) a.
proof: Proof. Proof using plusA multA invA divA cs A1. intros a b H' H'0. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a (invTerm (A:=A) invA (n:=n) b)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply zeroP_plusTermr with (1 := cs); auto. apply (eqT_trans A n) with (y := b); auto. apply zeroP_invTerm_zeroP with (1 := cs); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)