proposition: Lemma intersection_is_sup f x: fgraph f -> (allf f (partition_s ^~ x)) -> nonempty (domain f) -> least_upper_bound (coarser x) (range f) (intersection_partition f).
proof: Proof. move=> fgf alp nef. move: (intersection_is_partition fgf alp nef) => ip. move: (coarser_osr x) => [pa pb]. have aux: forall u, inc u (substrate (coarser x)) <-> partition_s u x. by move=> u; rewrite pb; apply:partitionsP. have aux2: sub (range f) (substrate (coarser x)). by move => t /(range_gP fgf) [u udf] ->; apply/aux;apply: alp. apply /(lubP pa aux2). split; first by split;[ apply/aux | move=> y; apply: intersection_is_sup_a]. move=> z [];rewrite aux => pzx zle. apply /coarser_gleP;split => // t tz. pose g u := select (sub t) (Vg f u). have gp u: inc u (domain f) -> sub t (g u) /\ inc (g u) (Vg f u). move=> udf;move: (zle _ (inc_V_range fgf udf)). move/coarser_gleP => [aa bb h]; move: (h _ tz) => [zz za zb]. apply: select_pr; first ex_tac. move => v1 v2 /= ha hb hc hd. move: (proj2 pzx _ tz) => [w wt]. case: ((proj2 (proj1 aa)) v1 v2 ha hc) => //. rewrite /disjoint=> dd; empty_tac1 w. have ai: (sub t (intersectionb (Lg (domain f) g))). move=> v vt; apply: setIb_i. move: nef => [y ydf]; exists (J y (Vg (Lg (domain f) g) y)). apply: fdomain_pr1; aww. by aw; move=> i idf; rewrite LgV//; apply: (proj1 (gp _ idf)). exists (intersectionb (Lg (domain f) g)); last by exact. apply /setC1_P; split; last first. move: (proj2 pzx _ tz) => [b bt]; move=> ie; empty_tac1 b. apply /funI_P. exists (Lg (domain f) g) => //; apply /setXb_P; split => //;aw; fprops. by move=> i idf; rewrite LgV//; case: (gp _ idf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)