proposition: Lemma inj_vK : cancel inj_v proj_v.
proof: Proof. move => v. rewrite /proj_v /inj_v /=. have P : enum_rank v < #|G| by []. case: insubP => [k _ /ord_inj -> /=|]; by rewrite ?P ?enum_rankK. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)