proposition: Lemma quot_bijE' (x: T): quot_bij^-1 (\pi x) = \pi h^-1 x.
proof: Proof. apply/eqquotP. rewrite -map_equivE. apply piK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)