proposition: Lemma permutationsP x E: inc x (permutations E) <-> bijection_prop x E E.
proof: Proof. split; first by move => /Zo_P [/functionsP [pa pb pc] pd]. move => [pa pb pc]; apply:Zo_i => //; apply/functionsP; split => //; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)