proposition: Lemma subset_tl (T : eqType) z (l : seq T) : {subset l <= z :: l}.
proof: Proof. move => x y. exact: mem_tail. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)