proposition: Lemma ex1_prop7 i j: gle rL i j -> lf_axiom (restr^~ (Vg Jf i)) (ex1_Fl j) (ex1_Fl i).
proof: Proof. move => lij; move: (prl_restr_canonical_ax (ex1_prop5 lij)). by rewrite (ex1_prop6a lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)