proposition: Lemma fsum_nat_const (e : {fset I}) a : \sum_(i <- e) a = #|` e| * a.
proof: Proof. by rewrite big_const_seq count_predT iter_addn_0 mulnC. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)