proposition: Lemma worder_rc_seg (r: relation) x: worder_rc r -> r x x -> worder_on (graph_on r (segmentr r x)) (segmentr r x).
proof: Proof. move => [pa pb] rxx; apply: (wordering_pr pa). move => a /(segmentrP pb rxx) [pc _]. by move: (pa) => [[_ _ rr] _]; move: (rr _ _ pc) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)