proposition: Lemma ordinalr_Mle r x y: worder_rc r -> r x y -> (ordinalr r x) <=o (ordinalr r y).
proof: Proof. move => pa px. move: (proj33 (proj1 (proj1 pa)) _ _ px) => [rxx ryy]. move: (proj1 (worder_rc_seg pa rxx)) (proj1 (worder_rc_seg pa ryy)) => ha hb. apply: order_cp2 => //. have ss: sub (segmentr r x) (segmentr r y). move => t /(segmentrP (proj2 pa) rxx)[sa sb]. move: (proj31 (proj1 (proj1 pa)) _ _ _ sa px) => ty. apply/(segmentrP (proj2 pa) ryy); split => //. move => ety; rewrite - ety in px. by move: (proj32_1 (proj1 pa) _ _ sa px). apply/(order_cp0 (proj1 ha) (proj1 hb)) => u v. by move /graph_on_P1 => [sa sb sc]; apply /graph_on_P1; split => //; apply: ss. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)