proposition: Lemma testbit_M : forall k n, le_o digits n -> testbit k n = false.
proof: Proof. simpl. intros. unfold testbit. replace (63 <=? n)%nat with true by lia. reflexivity. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR