proposition: Lemma minusP_inv : forall (p q l : list (Term A n)) (a b : Term A n), minusP (pX a p) (pX b q) l -> exists l1 : list (Term A n), ltT ltM b a /\ minusP p (pX b q) l1 /\ l = pX a l1 \/ ltT ltM a b /\ minusP (pX a p) q l1 /\ l = pX (invTerm (A:=A) invA (n:=n) b) l1 \/ eqT a b /\ (zeroP (A:=A) A0 eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) /\ minusP p q l \/ ~ zeroP (A:=A) A0 eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) /\ minusP p q l1 /\ l = pX (minusTerm (A:=A) minusA (n:=n) a b) l1).
proof: Proof. intros p q l a b H'; simple inversion H'. discriminate H. discriminate H0. rewrite <- H3; rewrite (pX_invl A n a2 b l2 q H2); rewrite (pX_invr A n l2 q a2 b H2); rewrite (pX_invl A n a1 a l1 p H1); rewrite (pX_invr A n l1 p a1 a H1). intros H'0 H'1; exists l3; left; split; [ idtac | split ]; auto. rewrite <- H4. intros H'0 H'1 H'2; exists l3; right; right. rewrite <- (pX_invl A n a2 b l2 q); try rewrite <- (pX_invl A n a1 a l1 p); auto. rewrite <- (pX_invr A n l2 q a2 b); try rewrite <- (pX_invr A n l1 p a1 a); auto. intros H'0 H'1 H'2; exists l3; right; right. rewrite <- H4. rewrite <- (pX_invl A n a2 b l2 q); try rewrite <- (pX_invl A n a1 a l1 p); auto. rewrite <- (pX_invr A n l2 q a2 b); try rewrite <- (pX_invr A n l1 p a1 a); auto. intros H'0 H'1; exists l3; right; left. rewrite <- (pX_invl A n a2 b l2 q); try rewrite <- (pX_invl A n a1 a l1 p); auto. rewrite <- (pX_invr A n l2 q a2 b); try rewrite <- (pX_invr A n l1 p a1 a); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)