proposition: Lemma wordering_pr r x: worder_r r -> {inc x, reflexive_r r} -> worder_on (graph_on r x) x.
proof: Proof. move=> [or wo] ar. have sg := (graph_on_sr ar). have gor := (order_from_rel x or). split=>//; split=>//. rewrite sg => s sx nes. have rs: {inc s, reflexive_r r} by move=> a /sx/ar. have sgs: substrate (graph_on r s) = s by rewrite graph_on_sr. move: (wo _ rs nes)=> [a []]; rewrite sgs => ais lea. have ss:sub s (substrate (graph_on r x)) by rewrite sg. exists a; split; first by rewrite iorder_sr. rewrite (iorder_sr gor ss) => y ys; aw. move: (lea _ ys) => /graph_on_P1 [pa pb pc]; apply/iorder_gle0P => //. by apply/graph_on_P1;split => //; apply: sx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)