proposition: Lemma intersection_is_sup2 u v x: partition_s u x -> partition_s v x -> least_upper_bound (coarser x)(doubleton u v)(intersection_partition2 u v).
proof: Proof. move=> pu pv;apply: lub_set2. apply: (proj1 (coarser_osr _)). by apply: intersection_is_sup2_a. by rewrite intersection_p2_comm; apply: intersection_is_sup2_a. move=> t /coarser_gleP [_ pt c1] /coarser_gleP [_ _ c2]. apply /coarser_gleP;split => //;first by apply intersection_is_partition2. move=> A At; move: (c1 _ At)(c2 _ At) => [b bu Ab] [c cv Ac]. have sA: sub A (b \cap c) by move=> w wA;apply: setI2_i; fprops. exists (b \cap c) => //; apply: Zo_i. apply /setI_covering2_P; exists b, c; split => //. move: ((proj2 pt) _ At) => [w /sA wA] /set1_P wne; empty_tac1 w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)