proposition: Lemma bijectionsP x y f: inc f (bijections x y) <-> bijection_prop f x y.
proof: Proof. split. by move /Zo_P => [/functionsP [_ sf tf]] bf. move=> [fa fb fc]; apply:Zo_i => //; apply /functionsP; split => //; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)