proposition: Lemma or_cut_segment_irrelevant r x Y (X := Zo (substrate r) (fun t => glt r x t)) (X' := Zo (substrate r) (fun t => gle r x t)): order r -> Y <> X -> Y <> X' -> (glt (or_cut_order r) X Y <-> glt (or_cut_order r) X' Y).
proof: Proof. move => or ha hb. move: (or_cut_segment x or)(or_cut_segmente x or). rewrite -/X -/X' => cx xy. split;move => [/or_cut_gleP [sa sb sc] sd]; split. + apply/or_cut_gleP; split => // t ty. by move: (sc _ ty) => /Zo_P [tst [lxt _]]; apply:Zo_i. + by apply:nesym. + apply/or_cut_gleP; split => // t ty. case: (inc_or_not x Y) => xY. case hb; apply: extensionality => // z zX. case: (equal_or_not x z) => exz; first by rewrite - exz. by move/Zo_P:zX => [za zb]; move: sb => [_ hh]; apply: (hh _ _ xY). move: (sc _ ty) => /Zo_P [tsr lxt]; apply/Zo_P; split => //; split => //. by dneg h; rewrite h. + by apply:nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)