proposition: Lemma or_cut_gleP r x y: gle (or_cut_order r) x y <-> [/\ ( or_cut r x), or_cut r y & sub y x].
proof: Proof. split. by move/opp_gleP => /sub_gleP [/or_cutsP sa /or_cutsP sb sc]; split. by move => [/or_cutsP sa /or_cutsP sb sc]; apply/opp_gleP /sub_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)