proposition: Lemma big_nat_mkfset (F : nat -> R) n : \sum_(0 <= i < n) F i = \sum_(i : [fset x in (iota 0 n)]) F (val i).
proof: Proof. rewrite -(big_map val xpredT) /=; apply/perm_big. apply/uniq_perm; rewrite ?iota_uniq //. rewrite map_inj_uniq /=; last apply/val_inj. by rewrite /index_enum -enumT enum_uniq. by move=> i; rewrite /index_enum -enumT -enum_fsetE in_fset /index_iota subn0. Qed.
imports: mathcomp(all_ssreflect all_algebra)