proposition: Theorem minusTerm_zeroP_r : forall a b : Term A n, zeroP (A:=A) A0 eqA (n:=n) a -> eqT a b -> eqTerm (A:=A) eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) (invTerm (A:=A) invA (n:=n) b).
proof: Proof. Proof using plusA multA divA cs A1. intros a b H' H0; 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); apply zeroP_plusTerml with (1 := cs); auto. apply (eqT_trans A n) with (y := b); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)