proposition: Lemma up_disjoint x y: (intersectionU2 U inc' x y = emptysetU U inc') <-> disjoint (f x) (f y).
proof: Proof. rewrite up_inter2; move:up_values => [-> _ _ _ _]. rewrite /disjoint; split => // h; first by move: (f_equal f h); rewrite fg fg. by rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)