proposition: Lemma testbit_true_nonneg': forall a i, 0 <= i -> 2 ^ i <= a < 2 ^ (i + 1) -> Z.testbit a i = true.
proof: Proof. intros. apply Z.testbit_true; [assumption|]. destruct H0 as [A B]. pose proof (pow2_pos i H) as Q. apply (Z.div_le_mono _ _ _ Q) in A. rewrite Z_div_same in A by lia. pose proof (Z.div_lt_upper_bound a (2 ^ i) 2 Q) as P. rewrite Z.mul_comm in P. replace i with (i + 1 - 1) in P by lia. rewrite <- pow2_times2 in P by lia. specialize (P B). replace (i + 1 - 1) with i in P by lia. replace (a / 2 ^ i) with 1 by lia. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith