proposition: Lemma image_of_covering f g: surjection g -> covering f (source g) -> covering (Lg (domain f) (fun w => Vfs g (Vg f w))) (target g).
proof: Proof. move=> [fg sg] [fgf cf]; split; first by fprops. move => x xtg; move: (sg _ xtg)=> [y ys vg]. move:(setUf_hi (cf _ ys)) => [z zsf yfz]. apply/setUb_P; aw; ex_tac; rewrite LgV // vg. apply/dirim_P; ex_tac; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)