proposition: Lemma piK (T: finType) (e: equiv_rel T) (x: T): e (repr (pi e x)) x.
proof: Proof. apply /eqquotP. by rewrite reprK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)