proposition: Lemma subset_catL (T : eqType) (h k : seq T) : {subset h <= h ++ k}.
proof: Proof. move => x H. by rewrite mem_cat H. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)