proposition: Lemma product_of_covering f g x y: covering f x -> covering g y -> covering (Lg ((domain f) \times (domain g)) (fun z => (Vg f (P z)) \times (Vg g (Q z)))) (x \times y).
proof: Proof. move=> [fgf c1] [fgg c2]; split; first by fprops. move => z /setX_P [zp px qy]. move /setUb_P: (c1 _ px) => [a asf pa]. move /setUb_P: (c2 _ qy) => [b bsg ab]. have pc: inc (J a b) ((domain f) \times (domain g)) by fprops. by apply/setUb_P;exists (J a b); aw;trivial; rewrite LgV //; aw;apply:setX_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)