proposition: Lemma ordinalr_Mlt (r:relation) x y: worder_rc r -> r x y -> x <> y -> (ordinalr r x) <o (ordinalr r y).
proof: Proof. move => pa px xny. move: (pa) => [[[rt ra rr] _] csr]. have [rxx ryy] := (rr _ _ px). move: (segmentrP csr rxx) (segmentrP csr ryy) => sx sy. have ss: sub (segmentr r x) (segmentr r y). move => t /sx [sa sb]. move: (rt _ _ _ sa px) => ty; apply/sy; split => //. dneg ety; rewrite - ety in px. exact: (ra _ _ sa px). move: (proj1 (worder_rc_seg pa rxx)) (proj1 (worder_rc_seg pa ryy)) => ha hb. have pb: sub (graph_on r (segmentr r x)) (graph_on r (segmentr r y)). apply/(order_cp0 (proj1 ha) (proj1 hb)) => u v. by move/graph_on_P1 => [sa sb sc]; apply /graph_on_P1; split => //; apply: ss. have pc: forall z, r z z -> substrate (graph_on r (segmentr r z)) = (segmentr r z). move => z rzz; apply :graph_on_sr => a /(segmentrP csr rzz) [xx _]. by move: (rr _ _ xx) => []. have xsy: inc x (segmentr r y) by apply /sy. apply: order_cp3 => //. split => // /(f_equal substrate). rewrite (pc _ rxx) (pc _ ryy) => h. by move: xsy; rewrite -h; move/sx =>[_]. rewrite (pc _ rxx); hnf; rewrite (pc _ ryy); split => //. move => a b /sx [sa sb] /graph_on_P1 [h1 h2 h3]; apply /sx. move: (rt _ _ _ h3 sa) => bx; split => // ebx. by rewrite ebx in h3; move: (ra _ _ sa h3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)