proposition: Lemma bij_quotE' (x: T2): bij_quot^-1 (\pi x) = \pi h_inv x.
proof: Proof. simpl. apply: h_inv_homo. by rewrite reprK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)