proposition: Lemma prl_r3_prop7 i j: gle prl_r3_nr i j -> lf_axiom (restr^~ i) (prl_r3_Fl j) (prl_r3_Fl i).
proof: Proof. move => lij; move: (prl_restr_canonical_ax (prl_r3_prop5 lij)). by rewrite (prl_r3_prop6a lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)