proposition: Lemma or_cut_P2 r B : total_order r -> sub B (substrate r) -> (or_cut r B <-> forall x y, inc x (substrate r -s B) -> inc y B -> glt r x y).
proof: Proof. move => [or tor] sa; split; last by apply/or_cut_prop2. move => [ua ub] x y /setC_P[xsr nb] yb. have nxy: x <> y by dneg h; ue. case: (tor _ _ xsr (sa _ yb)) => ha; first by split. case:nb; exact: (ub y x yb (conj ha (nesym nxy))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)