# Library binders_bullets

An example of declaration of notation with n-ary binders

Definition unique {A : Type} (P : A->Prop) (x:A) :=
P x /\ forall (x':A), P x' -> x=x'.

Notation "'exists' ! x .. y , p" :=
(ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
(at level 200, x binder, right associativity,
format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'")
: type_scope.

An example of use of n-ary "exists!" and bullets

Require Import Plus.

Lemma unique_sum_zero : exists! x y : nat, x + y = 0.
Proof.
exists 0. split.
- exists 0. split.
+ trivial.
+ symmetry; trivial.
- intros x' (y',(Hy',Huniq)). apply plus_is_O in Hy' as (->,_). trivial.
Qed.

An example of use of bullets and bracketed proofs

Require Import Arith.

Definition has_unique_least_element {A:Type} (R:A->A->Prop) (P:A->Prop) :=
exists! x, P x /\ forall x', P x' -> R x x'.

Lemma dec_inh_nat_subset_has_unique_least_element :
forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
(exists n, P n) -> has_unique_least_element le P.
Proof.
intros P Pdec (n0,HPn0).
assert
(forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
\/(forall n', P n' -> n<=n')).
{ induction n.
- right. intros n' Hn'. apply le_O_n.
- destruct IHn.
+ left; destruct H as (n', (Hlt', HPn')).
exists n'; split.
* apply lt_S; assumption.
* assumption.
+ destruct (Pdec n).
* left; exists n; split.
apply lt_n_Sn.
split; assumption.
* right.
intros n' Hltn'.
destruct (le_lt_eq_dec n n') as [Hltn| ->].
apply H; assumption.
assumption.
destruct H0 as []; assumption. }
destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
repeat split;
assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
Qed.