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