proposition: Lemma intersection_is_partition2 u v x: partition_s u x -> partition_s v x -> partition_s (intersection_partition2 u v) x.
proof: Proof. move=> ux vx; rewrite /intersection_partition2. split; first split; last by move => t /setC1_P/proj2/nonemptyP. set_extens t. move=> /setU_P [y ty] /setC1_P [] /setI_covering2_P [a [b [au bv yv]]] _. move: ux => [[<- _] _]; apply /setU_P; ex_tac. by move: ty; rewrite -yv; move /setI2_P => [ta _]. move=> tx; move: tx (tx); move: ux vx => [ [ {2} <- _] _] [[<- _] _]. move => /setU_P [y1 ty1 y1u] /setU_P [y2 ty2 y2u]. have ti: inc t (y1 \cap y2) by apply: setI2_i. apply /setU_P;exists (y1 \cap y2) => //. apply/setC1_P; split; first by apply /setI_covering2_P; exists y1, y2. by apply/nonemptyP; exists t. move=> a b /setC1_P [] /setI_covering2_P [a1 [b1 [a1u b1v]]] <- _ /setC1_P [] /setI_covering2_P [a2 [b2 [a2u b2v]]] <- _. apply: disjoint_pr1 => w /setI2_P [w1 w2] /setI2_P [w3 w4]. move:(proj2 (proj1 ux)) (proj2 (proj1 vx)) => ha hb. have ->: a1=a2 by case: (ha _ _ a1u a2u) => // h1; empty_tac1 w. have -> //: b1=b2 by case:(hb _ _ b1v b2v) => // d1; empty_tac1 w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)