proposition: Lemma quot_fun_can (T1 T2 : finType) (e1 : equiv_rel T1) (e2 : equiv_rel T2) (h1 : T1 -> T2) (h2 : T2 -> T1) : {homo h2 : x y / x = y %[mod e2] >-> x = y %[mod e1]} -> (forall x, h2 (h1 x) = x %[mod e1]) -> @cancel (quot e2) (quot e1) (quot_fun h1) (quot_fun h2).
proof: Proof. move => h2_hom h1_can x. rewrite /quot_fun -{2}[x]reprK -[\pi (repr x)]h1_can. apply: h2_hom. by rewrite reprK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)