proposition: Lemma existsb_case (P : pred bool) : [exists b, P b] = P true || P false.
proof: Proof. apply/existsP/idP => [[[|] -> //]|/orP[H|H]]; eexists; exact H. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)