proposition: Lemma testbit_false_nonneg: forall a i, 0 <= a < 2 ^ i -> 0 < i -> Z.testbit a (i - 1) = false -> a < 2 ^ (i - 1).
proof: Proof. intros. assert (2 ^ (i - 1) <= a < 2 ^ i \/ a < 2 ^ (i - 1)) as C by lia. destruct C as [C | C]; [exfalso|assumption]. assert (Z.testbit a (i - 1) = true); [|congruence]. replace i with (i - 1 + 1) in C at 2 by lia. apply testbit_true_nonneg'; lia. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith