proposition: Lemma bit_pred_1_lsl : forall n i , (n <? digits = true)%uint63 -> (bit (1 << n - 1) i)%uint63 = (to_Z i <? to_Z n)%Z.
proof: Proof. intros. rewrite bitE. rewrite sub_spec. rewrite Z.mod_small. rewrite lsl_1_spec by auto. replace (2 ^ φ (n)%uint63 - φ (1)%uint63)%Z with (Z.pred (2 ^ (to_Z n)))%Z by lia. rewrite <- Z.ones_equiv. apply Z.testbit_ones_nonneg. lia. lia. rewrite lsl_1_spec by auto. assert (2^0 <= 2 ^ to_Z n)%Z. { apply Z.pow_le_mono_r ; lia. } unfold wB, size. change (Z.of_nat 63) with 63%Z. assert (2^ to_Z n < 2 ^ 63)%Z. { apply Z.pow_lt_mono_r. lia. lia. lia. } lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR