proposition: Lemma mesym1E : 's_1 = \sum_(i < n) 'X_i.
proof: Proof. rewrite mesymE -big_set /=; set S := [set _ | _]. have ->: S = [set [set i] | i : 'I_n]. apply/eqP; rewrite eqEcard (card_imset _ set1_inj). rewrite card_draws /= !card_ord bin1 leqnn andbT. apply/subsetP=> /= s; rewrite inE => /cards1P /= [i {s}->]. by apply/imsetP; exists i. rewrite big_imset /=; last by move=> i1 i2 _ _; apply/set1_inj. by apply/eq_bigr=> i _; rewrite mesym1_set1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg