proposition: Lemma testbit_true_nonneg: forall a i, 0 <= a -> 0 <= i -> Z.testbit a i = true -> 2 ^ i <= a.
proof: Proof. intros. apply Z.testbit_true in H1; [|assumption]. pose proof (pow2_pos i H0). eapply Z.le_trans; [| apply (div_mul_undo_le a (2 ^ i)); lia]. replace (2 ^ i) with (1 * 2 ^ i) at 1 by lia. apply Z.mul_le_mono_nonneg_r; [lia|]. pose proof (Z.div_pos a (2 ^ i)). assert (a / 2 ^ i <> 0); [|lia]. intro E. rewrite E in H1. cbv in H1. discriminate H1. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith