proposition: Lemma permutation_rK E x y: inc x (permutations E) -> inc y (permutations E) -> (x \co y) \co (inverse_fun y) = x.
proof: Proof. move => ha hb; apply:compf_rK (permutation_coP ha hb). by move/permutationsP:hb => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)