proposition: Theorem uniq_opp: forall p1 p2, add p1 p2 = inf_elt -> p2 = opp p1.
proof: Proof. intros p1 p2; kcase p1 p2. intros p H; rewrite H; auto. intros; subst; discriminate. intros; subst; discriminate. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith