proposition: Lemma lopp_spec_low: forall k m, (forall p, (p < m)%nat -> testbit k p = false) -> testbit k m = true -> forall p, (p < m)%nat -> testbit (Uint63.opp k) p = false.
proof: Proof. intros. assert (IS : is_set k m). { unfold is_set ; auto. } assert (MSMALL := is_set_small k m IS). apply is_set_decomp in IS. rewrite IS. rewrite opp_mask by (unfold digits; lia). unfold testbit. replace (int_of_nat (Init.Nat.min p 62)) with (int_of_nat p) by lia. rewrite Uint63.lor_spec. rewrite bit_lsl. rewrite bit_lsl. rewrite bit_1. repeat elim_if ; lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR