proposition: Lemma or_cut_gle_least r : least (or_cut_order r) (substrate r) .
proof: Proof. have [or sr]:= (or_cut_osr r). have pc: or_cut r (substrate r) by split => // x y _ h; order_tac. have pf:inc (substrate r) (or_cuts r) by apply/or_cutsP. by hnf;rewrite sr; split => // x /or_cutsP [xsrp xp]; apply/ or_cut_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)