proposition: Lemma lsl_1_spec : forall n, (n <? digits = true)%uint63 -> (φ (1 << n)%uint63 = 2 ^ to_Z n)%Z.
proof: Proof. intros. rewrite lsl_spec. rewrite Z.mod_small. lia. replace (φ (1)%uint63 * 2 ^ φ (n)%uint63)%Z with (2^ to_Z n)%Z by lia. split. apply Z.pow_nonneg. lia. unfold wB. unfold size. apply Z.pow_lt_mono_r. lia. lia. unfold digits in *; lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR