proposition: Lemma all_cons (T : eqType) (P : T -> Prop) a (s : seq T) : {in a::s, forall x, P x} <-> P a /\ {in s, forall x, P x}.
proof: Proof. split => [A|[A B]]; last by move => x /predU1P [-> //|]; apply: B. by split => [|b Hb]; apply: A; rewrite !inE ?eqxx ?Hb. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)