proposition: Lemma not_int_lsl : forall k m, (m <? digits = true)%uint63 -> (not_int ((k >> (m+1)) << (m+1) lor (1 << m)) = (((not_int k) >> (m+1) << (m+1)) lor (1 << m - 1)))%uint63.
proof: Proof. intros. apply bit_ext'; intros. rewrite! bit_not_int by auto. rewrite! Uint63.lor_spec. rewrite bit_pred_1_lsl by auto. rewrite bit_lsl. rewrite! bit_lsr. rewrite! bit_lsl. rewrite bit_lsr. rewrite bit_not_int. replace ((m + 1 + (n - (m + 1))))%uint63 with n by lia. rewrite bit_1. repeat elim_if. intuition try lia. destruct (bit k n); lia. zify. lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR