proposition: Lemma or_cut_segmente_cp r x y (X := Zo (substrate r) (fun t => gle r x t)) (Y := Zo (substrate r) (fun t => gle r y t)): total_order r -> inc x (substrate r) -> inc y (substrate r) -> (glt r x y <-> glt (or_cut_order r) X Y).
proof: Proof. move => [or tor] xsr ysr;split. move => [lxy nxy]; split. apply/or_cut_gleP; split. + apply:(or_cut_segmente _ or). + apply:(or_cut_segmente _ or). + move => t /Zo_P [ta tb]; apply/Zo_P; split => //; order_tac. dneg eXY. have: inc x X by apply /Zo_P; split => //; order_tac. rewrite eXY; move /Zo_hi => ha; order_tac. move => [/or_cut_gleP [[sa sb] [sc sd]] se] XY. have xy: x <> y by dneg h; rewrite /X/Y h. split => //; case: (tor _ _ xsr ysr) => // cxy. have: inc y Y by apply /Zo_P; split => //; order_tac. move/se => /Zo_hi ha; case xy; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)