proposition: Lemma ex4_function_f_ax a b: gle r a b -> lf_axiom (ex4_function_fv a) (ex4_setEi b) (ex4_setEi a).
proof: Proof. move=> lab x /Zo_P[xF rx]; rewrite - rx in lab. by move:(ex4_function_f_prop1 xF lab) => h; apply/Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)