proposition: Lemma is_set_eq : forall k m, is_set k m -> exists n, n = int_of_nat m /\ (n <? digits = true)%uint63 /\ is_set_int k n.
proof: Proof. intros. assert (SM := is_set_small _ _ H). unfold is_set, is_set_int in *. destruct H. exists (int_of_nat m). split_and; intros. - reflexivity. - unfold digits ; lia. - unfold testbit in H. rewrite <- H with (p := nat_of_int p). replace (63 <=? nat_of_int p) with false by (unfold nat_of_int in* ; lia). f_equal. unfold nat_of_int ; lia. unfold nat_of_int ; lia. - unfold testbit in H0. rewrite <- H0. destruct (63 <=? m) ; congruence. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR