proposition: Lemma is_set_small : forall k m, is_set k m -> m < 63.
proof: Proof. intros. unfold is_set in *. destruct H. unfold testbit in *. destruct (63 <=? m) eqn:EQ ; lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR