proposition: Lemma eq_image (A B : {pred T}) (f g : T -> T') : A =i B -> f =1 g -> image f A = image g B.
proof: Proof. by move=> eqAB eqfg; rewrite /image_mem (eq_enum eqAB) (eq_map eqfg). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)