proposition: Lemma last_mem (T : eqType) (x : T) (s : seq T) : x \in s -> last x s \in s.
proof: Proof. by elim/last_ind: s => // s y _ _; rewrite last_rcons mem_rcons mem_head. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)