proposition: Lemma or_cut_tor r: total_order r -> total_order (or_cut_order r).
proof: Proof. move: (or_cut_osr r) => [or sr] tor. split => // x y; rewrite sr => xc yc. suff: sub x y \/ sub y x. by case => h; [right | left]; apply/opp_gleP; apply/sub_gleP. move/or_cutsP: xc => [xsr cx]. move/or_cutsP: yc => [ysr cy]. case(p_or_not_p (sub x y)) => h; first by left. have[a ax nay]: exists2 a, inc a x & ~inc a y. ex_middle bad; case h => b bx; ex_middle iby; case bad; ex_tac. right => b iby. case: (equal_or_not a b) => eab; first by case:nay; rewrite eab. case: (proj2 tor _ _ (xsr _ ax) (ysr _ iby)). by move => lab; move:(cx _ _ ax (conj lab eab)). move => lab; case: nay; exact: (cy b a iby (conj lab (nesym eab))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)