proposition: Lemma intersection_p2_comm u v: (intersection_partition2 u v) = (intersection_partition2 v u).
proof: Proof. set_extens t; move /setC1_P => [] /setI_covering2_P [a [b [au bv it]]] net; apply /setC1_P; split => //; apply /setI_covering2_P; by exists b, a; rewrite setI2_C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)