proposition: Lemma lf_surjective f a b: lf_axiom f a b -> (forall y, inc y b -> exists2 x, inc x a & y = f x) -> surjection (Lf f a b).
proof: Proof. move=> ta prop; split; first by apply: lf_function. by aw; move=> y yt; case: (prop _ yt)=> x xa fy; ex_tac; rewrite LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)