proposition: Lemma collectivising_srel_ord_seg (r:relation) : (forall x y, r x y -> x <=o y) -> forall x, r x x -> segmentr r x = Zo x (fun z => r z x).
proof: Proof. move => ro x rxx. have ox:=(proj31 (ro _ _ rxx)). have cr:=(collectivising_srel_ord ro). set_extens t. move /(segmentrP cr rxx) => [pa pb]; apply: Zo_i; last exact:pa. by apply/(oltP ox); split => //; apply: ro. move => /Zo_P[pa pb]; apply /(segmentrP cr rxx); split => //. by move=> tx; case: (ordinal_decent ox pa); rewrite {2} tx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)