proposition: Lemma prl_r3_trans i j k: gle prl_r3_nr i j -> gle prl_r3_nr j k -> gle prl_r3_nr i k.
proof: Proof. move => ha hb; move: (sub_osr prl_r3_nI) => [[_ _ tr _ ] _]. apply: (tr _ _ _ ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)