proposition: Theorem uniq_zero: forall p1 p2, add p1 p2 = p2 -> p1 = inf_elt.
proof: Proof. intros p1 p2; kcase p1 p2. intros p; case p; simpl; auto; intros; discriminate. intros. subst p1 p2; injection H8; intros H9 H10. generalize (Keq_minus_eq_inv H7); clear H7; intros H7. ring_simplify [H9 H10] in H7. case (Kmult_integral H7); auto; intros H11. case Kdiff_2_0; auto. case H4; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p3 x3 y3 H3 l Hp1 Hp2 Hp3 Hp3b Hd Hl Hx3 Hy3 Hp. apply False_ind. subst p2; subst p3; injection Hp; clear p1 Hp1 Hp Hp3b; intros. case (@aux1 x1 y1 x2 y2); auto. generalize (Keq_minus_eq_inv Hy3); rewrite Hl; rewrite H; rewrite H0; clear Hy3; intros Hy3. field_simplify_eq in Hy3; auto. assert (HH: 2 * y2 * (x2 - x1) = 0). rewrite Hy3; ring. clear Hy3; rename HH into Hy3. case (Kmult_integral Hy3); auto; clear Hy3; intros Hy3. case (Kmult_integral Hy3); auto; clear Hy3; intros Hy3. case Kdiff_2_0; auto. case Hd. symmetry; apply Keq_minus_eq; auto. rewrite <- Hl; rewrite <- Hx3; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith