proposition: Lemma intersection_is_sup2_b E u v: partition_s u E -> partition_s v E -> sup (coarser E) u v = (intersection_partition2 u v).
proof: Proof. move: (coarser_osr E) => [pa pb] pu pv. have i2 :=(intersection_is_sup2 pu pv). have hs: (has_supremum (coarser E) (doubleton u v)). by exists (intersection_partition2 u v). have sd: (sub (doubleton u v) (substrate (coarser E))). by move => t; rewrite pb;case/set2_P => ->; apply /partitionsP. by apply: (supremum_unique pa (supremum_pr1 _ hs) i2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)