proposition: Lemma permutation_Si E x: inc x (permutations E) -> inc (inverse_fun x) (permutations E).
proof: Proof. by move/permutationsP => /inverse_bij_bp /permutationsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)