proposition: Theorem minusP_inv3b : forall (a b : Term A n) (p q s : list (Term A n)), eqT a b -> ~ zeroP (A:=A) A0 eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) -> minusP (pX a p) (pX b q) s -> s = pX (minusTerm (A:=A) minusA (n:=n) a b) (minuspf p q).
proof: Proof. Proof using os. intros a b p q s Eqd Z0 H'; inversion_clear H'. absurd (ltT ltM b a); auto. apply ltT_not_eqT; auto; apply eqT_sym; auto. case Z0; auto. apply pX_inj; auto. apply uniq_minusp with (l := (p, q)); auto. absurd (ltT ltM a b); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)