proposition: Lemma permutation_if_inj E f: finite_set E -> function_prop f E E -> injection f -> inc f (permutations E).
proof: Proof. move => fse [ff sf tf] ijf; apply/permutationsP; split=> //. by apply: bijective_if_same_finite_c_inj => //; rewrite sf // tf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)