proposition: Lemma pi_surj (T : finType) (e : equiv_rel T) : forall x, x \in codom (pi e).
proof: Proof. move => y. by rewrite -[y]reprK codom_f. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)