proposition: Lemma inv_image_of_covering f g: function g -> covering f (target g) -> covering (Lg(domain f) (fun w => Vfi g (Vg f w))) (source g).
proof: Proof. move=> fg [fgf cf]; split; first by fprops. move => x xs; apply/setUb_P; aw. have Wt: (inc (Vf g x) (target g)) by fprops. move /setUb_P: (cf _ Wt) => [y ysf Wf]; ex_tac; rewrite LgV //. apply/iim_fun_P; ex_tac; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)