proposition: Lemma testbit_spec: forall k1 k2, (forall n, testbit k1 n = testbit k2 n) -> k1 = k2.
proof: Proof. intros. unfold testbit in *. apply Uint63.bit_ext;auto ; intros. specialize (H (Z.to_nat (Uint63.to_Z n))). destruct (63 <=? Z.to_nat (Uint63.to_Z n)) eqn:EQ. - assert (Uint63.leb Uint63.digits n = true). { unfold Uint63.digits. lia. } rewrite Uint63.bit_M by assumption. rewrite Uint63.bit_M by assumption. reflexivity. - assert ( int_of_nat (Z.to_nat (Uint63.to_Z n)) = n) by (unfold int_of_nat ; lia). congruence. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR