proposition: Lemma permutation_coP E x y: inc x (permutations E) -> inc y (permutations E) -> (x \coP y).
proof: Proof. move=> /permutationsP [[[fy _] _] sx _] /permutationsP [[[h _] _] _ ty]. by split => //; rewrite ty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)