proposition: Lemma testbit_0 : forall a n, (0 <= n)%Z -> Z.testbit a n = ((a / 2 ^ n) mod 2 =? 1)%Z.
proof: Proof. intros. generalize (Z.testbit_true a n H). destruct (Z.testbit a n); intuition. - rewrite H0. reflexivity. - assert ((a / 2 ^ n) mod 2 = 0 \/ a / 2 ^ n mod 2 = 1)%Z. clear. lia. destruct H0. rewrite H0. reflexivity. intuition congruence. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR