fact: Definition bij_double_F2_fun F G a b f g := let fi := inverse_fun f in let gi := inverse_fun g in let H := (G\times F \cup G\times G) \cup F \times G in let alpha := fun x y => J a (Vf fi (J x (Vf gi y))) in let beta := ( fun y => (Yo (inc y F) (J a y) (J b (Vf gi y)))) in let gamma := fun x y => J b (Vf fi (J (Vf gi x) (Vf fi (beta y)))) in let f2:= fun p => Vf g (Vf fi (Yo (inc (P p) F) (alpha (P p) (Q p)) (gamma (P p) (Q p)))) in let f3 := (cantor_bernstein_bij G H (Lf (J a) G H) (Lf f2 H G)) in let f4 := (fun x => Yo (inc x F) (Vf f x) (Vf f3 x)) in Lf f4 (F \cup G) (coarse (F\cup G)).
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)