proposition: Lemma or_cut_supinf r X: order r -> (forall x, inc x X -> or_cut r x) -> (or_cut r (union X) /\ or_cut r (intersection X)).
proof: Proof. move => sa sb; split. split; first by apply: setU_s2 => y /sb []. move => x y /setU_P [z za zb] zc; apply/setU_P; ex_tac. by move:(sb _ zb) => [ca cb]; apply: (cb _ _ za zc). case: (emptyset_dichot X) => xE. move:(proj1 (or_cut_gle_greatest r)). by rewrite (proj2 (or_cut_osr r)) xE setI_0; move => /Zo_hi. move:(xE) => [u uX]. split; first by move => t ti; exact:(proj1 (sb _ uX) _ (setI_hi ti uX)). move => x y xi h; apply/(setI_P xE) => z zX. have xz: inc x z by move/(setI_P xE):xi => H; apply:H. exact:(proj2 (sb _ zX) x y xz h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)