proposition: Lemma interp_spec: forall m n, is_mask m n -> forall p, testbit (interp m) p = true <-> (p < n)%nat.
proof: Proof. intros. apply mask_spec in H. destruct (63 <=? n) eqn:N; [tauto|]. subst. unfold testbit. destruct (63 <=?p) eqn:EQ. - lia. - assert (NS : n <= 62) by lia. assert (NP : p <= 62) by lia. rewrite <- Nat.ltb_lt. apply eqb_iff. set (Q:= fun n p => Bool.eqb (bit (interp (one << int_of_nat n)) (int_of_nat p)) (p <? n)). change (Q n p = true). eapply (forall_2n_correct _ 62 62);auto. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR