fact: Definition ex5_coherent1 J x := [/\ ex5_fneI J, ex5_prodG J x, forall i j, inc i J -> inc j J -> gle (psr S) i j -> Vg x i = Vf (ex5_f i j) (Vg x j) & forall k, ex5_upper_bd J k -> nonempty ((Vg Gf k) \cap (ex5_Y J k x))].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)