proposition: Lemma or_cut_prop2 r B : order r -> sub B (substrate r) -> (forall x y, inc x (substrate r -s B) -> inc y B -> glt r x y) -> or_cut r B.
proof: Proof. move => or sa sb; split => // x y xb lxy; ex_middle xne. have h: inc y ((substrate r) -s B) by apply/setC_P; split => //; order_tac. move:(sb y x h xb)=> [ha _]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)