proposition: Lemma lf_bijective f a b: lf_axiom f a b -> (forall u v, inc u a -> inc v a -> f u = f v -> u = v) -> (forall y, inc y b -> exists2 x, inc x a & y = f x) -> bijection (Lf f a b).
proof: Proof. by move => ta pi ps; split; [apply: lf_injective| apply: lf_surjective]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)