proposition: Theorem uniq_plusp : forall l l3 l4, plusP (fst l) (snd l) l3 -> plusP (fst l) (snd l) l4 -> l3 = l4.
proof: Proof. Proof using os. intros l; pattern l in |- *. apply well_founded_ind with (1 := wf_lessP A n). intros (l1, l2); simpl in |- *. case l1; clear l1. intros H' l3 l4 H'0; inversion_clear H'0; intros H'2; inversion_clear H'2; auto. case l2; clear l2. simpl in |- *; intros n0 l0 H' l3 l4 H'0 H'2; inversion H'2; inversion H'0; auto. simpl in |- *; intros n2 l2 n1 l1 Induc l3 l4 Hl3 Hl4. case (plusP_inv l1 l2 l4 n1 n2); auto. intros x H'; elim H'; [ intros H'0; elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; rewrite H'4; clear H'2 H'0 H' | intros H'0; clear H' ]. case (plusP_inv l1 l2 l3 n1 n2); auto. intros x0 H'; elim H'; [ intros H'0; elim H'0; intros H'2 H'5; elim H'5; intros H'6 H'7; rewrite H'7; clear H'5 H'0 H' | intros H'0; clear H' ]; auto. apply pX_inj; auto. apply Induc with (y := (l1, n2 :: l2)); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto. elim H'0; [ intros H'; elim H'; intros H'2 H'5; clear H' H'0 | intros H'; clear H'0 ]. absurd (ltT ltM n1 n2); auto. elim H'; intros H'0 H'2; try exact H'0; clear H'. absurd (eqT n2 n1); auto. apply (eqT_sym A n n1); auto. elim H'0; [ intros H'; elim H'; intros H'1 H'2; elim H'2; intros H'3 H'4; rewrite H'4; clear H'2 H' H'0 | intros H'; clear H'0 ]. case (plusP_inv l1 l2 l3 n1 n2); auto. intros x0 H'; elim H'; [ intros H'0; elim H'0; intros H'2 H'5; clear H'0 H' | intros H'0; clear H' ]. absurd (ltT ltM n1 n2); auto. elim H'0; [ intros H'; elim H'; intros H'2 H'5; elim H'5; intros H'6 H'7; rewrite H'7; clear H'5 H' H'0 | intros H'; clear H'0 ]. apply pX_inj; auto. apply Induc with (y := (pX n1 l1, l2)); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. elim H'; intros H'0 H'2; try exact H'0; clear H'. absurd (eqT n1 n2); auto. elim H'; intros H'0 H'1; try exact H'0; clear H'. case (plusP_inv l1 l2 l3 n1 n2); auto. intros x0 H'; elim H'; [ intros H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2 H' | intros H'2; clear H' ]. absurd (eqT n2 n1); auto. apply (eqT_sym A n n1); auto. elim H'2; [ intros H'; elim H'; intros H'3 H'4; try exact H'3; clear H' H'2 | intros H'; clear H'2 ]. absurd (eqT n1 n2); auto. elim H'; intros H'2 H'3; elim H'3; [ intros H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4 H'3 H' | intros H'4; clear H'3 H' ]. elim H'1; [ intros H'; clear H'1 | intros H'; elim H'; intros H'3 H'4; apply H'3 || elim H'3; clear H' H'1 ]; auto. elim H'; intros H'1 H'3; clear H'. apply Induc with (y := (l1, l2)); auto; red in |- *; simpl in |- *; auto. simpl in |- *; auto with arith. elim H'4; intros H' H'3; elim H'3; intros H'5 H'6; rewrite H'6; clear H'3 H'4. elim H'1; [ intros H'3; clear H'1 | intros H'3; elim H'3; intros H'4 H'7; elim H'7; intros H'8 H'9; rewrite H'9; clear H'7 H'3 H'1 ]. elim H'3; intros H'1 H'4; try exact H'1; clear H'3. apply H' || elim H'; try assumption. apply pX_inj; auto. apply Induc with (y := (l1, l2)); auto. red in |- *; red in |- *; simpl in |- *; auto with arith. Qed.
imports: Coq(Arith) Buchberger(LetP)