proposition: Lemma ex4_function_f_fun a b: gle r a b -> function_prop (ex4_function_f (J a b)) (ex4_setEi b) (ex4_setEi a).
proof: Proof. rewrite /ex4_function_f;move => lab; saw; apply: lf_function. by move => x; apply: ex4_function_f_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)