proposition: Lemma quot_bijE (x: S): quot_bij (\pi x) = \pi h x.
proof: Proof. simpl. apply /eqquotP. rewrite map_equivE 2!bijK. apply piK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)