proposition: Lemma exercise1_5: emptyset = choose (fun X => ~ (inc (rep X) X)).
proof: Proof. pose p := fun z => ~ inc (rep z) z. have pe: p emptyset by exact: in_set0. move:(choose_pr (ex_intro p emptyset pe)) => pcp. case:(emptyset_dichot (choose p)) => // ney; by move: (rep_i ney). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)