proposition: Lemma permutation_lK' E x y: inc x (permutations E) -> inc y (permutations E) -> x \co ( (inverse_fun x) \co y) = y.
proof: Proof. move => ha hb. move/permutationsP:(ha) => [[[/ifun_involutive hc _] _] _ _]. rewrite -{1} hc;apply:(permutation_lK (permutation_Si ha) hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)