proposition: Lemma intersection_is_sup2_a u v x: partition_s u x -> partition_s v x -> gle (coarser x) u (intersection_partition2 u v).
proof: Proof. move=> pu pv; apply /coarser_gleP; split => //. by apply: intersection_is_partition2. move=> y /Zo_P [] /setI_covering2_P [a [b [au bv h]]] _. ex_tac; rewrite -h;apply: subsetI2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)