bitsum: try removing positivity constraint on key_size

[tahina-pro]

everparse/src/lowparse/LowParse.Spec.BitSum.fst

Line 21 in 452f1fe

(key_size: nat { key_size > 0 /\ key_size <= bitsum'_size /\ bitsum'_size <= tot }) -> // key_size made positive because F* cannot prove that (payload _) is a smaller term wrt. << without FStar.WellFounded.axiom1_dep //NS: TODO: please check this comment

Thank you @nikswamy for pointing this out. For now I will leave it as is, for the sake of merging your changes into master, CI permitting.
Later I will separately investigate whether I can remove that restriction on key_size, and if not, I will update the comment accordingly.

Originally posted by @tahina-pro in #38 (comment)

[tahina-pro]

I hope this constraint can be lifted thanks to FStarLang/FStar#2205, which should allow me to correctly perform structural recursion on bitsum_t