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