proposition: Lemma sumn_flatten (ss : seq (seq nat)) : sumn (flatten ss) = sumn (map sumn ss).
proof: Proof. by elim: ss => // s ss /= <-; apply: sumn_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)