proposition: Lemma intersection_is_sup_a f x y: fgraph f -> (allf f (partition_s ^~ x)) -> inc y (range f) -> gle (coarser x) y (intersection_partition f).
proof: Proof. move=> fgf alp /(range_gP fgf) [z zdf ->]. have ne: nonempty (domain f) by exists z. apply /coarser_gleP; split;fprops; first by apply: intersection_is_partition. move=> a /setC1_P [] /funI_P [t zt h] _. move: zt => /setXb_P [fgt dt VV]; move: (VV _ zdf) => aux. ex_tac; rewrite h; move=> w wi; apply: (setIb_hi wi); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)