proposition: Lemma sumn_bound n (s : seq nat) : (forall x, x \in s -> x <= n) -> sumn s <= n * size s.
proof: Proof. elim: s => //= m s IHs H. rewrite mulnS leq_add ?H ?IHs ? mem_head //. move => x Hx. by rewrite H //= in_cons Hx. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)