proposition: Theorem plusP_com : forall p q r s, plusP p q r -> plusP q p s -> eqP A eqA n r s.
proof: Proof. Proof using os multA minusA ltM_dec invA eqA_dec divA cs A1. intros p q r s H'; generalize s; elim H'; clear s H'; auto. intros l1 s H'; try assumption. rewrite (pO_plusP_inv2 l1 s); auto. intros l1 s H'; rewrite (pO_plusP_inv1 l1 s); auto. intros a1 a2 l1 l2 l3 H' H'0 H'1 s H'2. rewrite (plusP_inv2 a2 a1 l2 l1 s); auto. intros a1 a2 l1 l2 l3 H' H'0 H'1 H'2 s R. rewrite (plusP_inv3a a2 a1 l2 l1 s); auto. apply (eqT_sym A n a1); auto. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a1 a2); auto. apply plusTerm_com with (1 := cs); auto. intros a1 a2 l1 l2 l3 H' H'0 H'1 H'2 s H'3. rewrite (plusP_inv3b a2 a1 l2 l1 s); auto. apply eqpP1; auto; apply plusTerm_com with (1 := cs); auto. apply (eqT_sym A n a1); auto. red in |- *; intros H'4; apply H'2. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a2 a1); auto. apply plusTerm_com with (1 := cs); auto. apply (eqT_sym A n); auto. intros a1 a2 l1 l2 l3 H' H'0 H'1 s H'2. rewrite (plusP_inv1 a2 a1 l2 l1 s); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)