proposition: Lemma sum_nat_const n : \sum_(i in A) n = #|A| * n.
proof: Proof. by rewrite big_const iter_addn_0 mulnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)