proposition: Lemma bounded_iff_bits k n : 0 ≤ k → -2^k ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0).
proof: Proof. intros Hk. case_bool_decide; [ | rewrite <-bounded_iff_bits_nonneg; lia]. assert(n = - Z.abs n)%Z as -> by lia. split. { intros [? _] l Hl. rewrite Z.bits_opp, negb_true_iff by lia. apply bounded_iff_bits_nonneg with k; lia. } intros Hbit. split. - rewrite <-Z.opp_le_mono, <-Z.lt_pred_le. apply bounded_iff_bits_nonneg; [lia..|]. intros l Hl. rewrite <-negb_true_iff, <-Z.bits_opp by lia. by apply Hbit. - etrans; [|apply Z.pow_pos_nonneg]; lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)