proposition: Lemma natnseq0P s : reflect (s = nseq (size s) 0) (sumn s == 0).
proof: Proof. apply: (iffP idP) => [|->]; last by rewrite sumn_nseq. by elim: s => //= x s IHs; rewrite addn_eq0 => /andP[/eqP-> /IHs <-]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)