proposition: Lemma signed_bounds_to_sz_pos: forall sz n, - 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) -> 0 < sz.
proof: Proof. intros. assert (0 < sz \/ sz - 1 < 0) as C by lia. destruct C as [C | C]; [assumption|exfalso]. rewrite Z.pow_neg_r in H by assumption. lia. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith