proposition: Lemma unique_existence : forall (A:Type) (P:A->Prop), ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
proof: Proof. intros A P; split. - intros ((x,Hx),Huni); exists x; red; auto. - intros (x,(Hx,Huni)); split. + exists x; assumption. + intros x' x'' Hx' Hx''; transitivity x. * symmetry; auto. * auto. Qed.
imports: Notations Ltac