proposition: Lemma opp_mask : forall k m, (m <? digits = true)%uint63 -> (- ((k >> (m + 1)) << ( m + 1) lor 1 << m) = (((not_int k) >> (m+1)) << (m+1)) lor ((1 << m)))%uint63.
proof: Proof. intros. rewrite opp_spec. rewrite! not_int_lsl by auto. repeat rewrite <- bit_add_or. zify. lia. - intros. rewrite bit_lsl in H1. rewrite bit_1 in H1. rewrite bit_lsl in H0. rewrite bit_lsr in H0. revert H0 H1. repeat elim_if. intuition try lia. - intros. rewrite bit_pred_1_lsl in H1 by lia. rewrite bit_lsl in H0. revert H0 H1. elim_if; intuition try lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR