proposition: Lemma plusP_inv : forall p q l (a b : Term A n), plusP (pX a p) (pX b q) l -> exists l1 : _, ltT ltM b a /\ plusP p (pX b q) l1 /\ l = pX a l1 \/ ltT ltM a b /\ plusP (pX a p) q l1 /\ l = pX b l1 \/ eqT a b /\ (zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) /\ plusP p q l \/ ~ zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) /\ plusP p q l1 /\ l = pX (plusTerm (A:=A) plusA (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 _ _ a2 b l2 q H2); rewrite (pX_invr _ _ l2 q a2 b H2); rewrite (pX_invl _ _ a1 a l1 p H1); rewrite (pX_invr _ _ l1 p a1 a H1). intros H'0 H'1; exists l3; left; split; [ idtac | split; [ try assumption | idtac ] ]; auto. rewrite <- H3. intros H'0 H'1 H'2; exists l3; right; right. rewrite <- (pX_invl _ _ a2 b l2 q H3); rewrite <- (pX_invl _ _ a1 a l1 p H2); auto. rewrite <- (pX_invr _ _ l2 q a2 b H3); rewrite <- (pX_invr _ _ l1 p a1 a H2); auto. rewrite <- H4; auto. intros H'0 H'1 H'2; exists l3; right; right. rewrite <- (pX_invl _ _ a2 b l2 q H3); rewrite <- (pX_invl _ _ a1 a l1 p H2); auto. rewrite <- (pX_invr _ _ l2 q a2 b H3); rewrite <- (pX_invr _ _ l1 p a1 a H2); auto. intros H'0 H'1; exists l3; right; left; split; [ idtac | split; [ try assumption | idtac ] ]; auto. rewrite <- (pX_invl _ _ a2 b l2 q H2); rewrite <- (pX_invl _ _ a1 a l1 p H1); auto. rewrite <- (pX_invl _ _ a1 a l1 p H1); rewrite <- (pX_invr _ _ l2 q a2 b H2); rewrite <- (pX_invr _ _ l1 p a1 a H1); auto. rewrite <- H3; rewrite <- (pX_invl _ _ a2 b l2 q H2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)