proposition: Lemma permutation_A E x y z: inc x (permutations E) -> inc y (permutations E) -> inc z (permutations E) -> x \co (y \co z) = (x \co y) \co z.
proof: Proof. move=> ha hb hc;apply: (compfA (permutation_coP ha hb)(permutation_coP hb hc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)