proposition: Lemma bool_two: bij bool (unit+unit).
proof: Proof. exists (fun b => if b then inr tt else inl tt) (fun x => match x with inl _ => false | inr _ => true end). all: abstract by repeat case. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)