proposition: Lemma land_spec: forall n k1 k2, testbit (Uint63.land k1 k2) n = testbit k1 n && testbit k2 n.
proof: Proof. intros. unfold testbit. rewrite Uint63.land_spec. destruct (63 <=? n) eqn:T; reflexivity. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR