proposition: Lemma permutation_id E: inc (identity E) (permutations E).
proof: Proof. move:(identity_prop E) => [_ pa pb]. apply/permutationsP;split => //; apply: identity_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)