proposition: Lemma permutation_Sc E x y: inc x (permutations E) -> inc y (permutations E) -> inc (x \co y) (permutations E).
proof: Proof. move=> /permutationsP xp /permutationsP yp; apply /permutationsP. apply: (compose_bp yp xp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)