proposition: Lemma prl_ne2_sigma_osr: order_on prl_ne2_sigma_order prl_ne2_sigma.
proof: Proof. have ha u: inc u prl_ne2_sigma -> prl_ne2_sigma_le u u. move => _ i _; fprops. have hb:=(graph_on_sr ha). split => //;apply: order_from_rel1 => //. move => j i k pa pb u ui; exact:(sub_trans (pb _ ui) (pa _ ui)). move => u v /Zo_P[ /setXb_P [fga da _] _] /Zo_P[ /setXb_P [fgb db _] _]. move => luv lvu; apply:fgraph_exten => //; rewrite da //. rewrite FS_domain => i iI; apply: (extensionality (lvu _ iI) (luv _ iI)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)