proposition: Lemma or_cut_gle_greatest r : greatest (or_cut_order r) emptyset.
proof: Proof. have [or sr]:= (or_cut_osr r). have pc: or_cut r emptyset by split => x; [move/in_set0 | move => y /in_set0]. have pf:inc emptyset (or_cuts r) by apply/or_cutsP. hnf;rewrite sr; split => // x /or_cutsP xc; apply/ or_cut_gleP; split => //. exact:sub0_set. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)