proposition: Lemma lopp_spec_high: forall k m, (forall p, (p < m)%nat -> testbit k p = false) -> testbit k m = true -> forall p, (p > m)%nat -> ~ le_o digits p -> testbit (Uint63.opp k) p = negb (testbit k p).
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. clear IS. simpl in H2. rewrite opp_mask by (unfold Uint63.digits; lia). unfold testbit. replace (63 <=?p)%nat with false by lia. rewrite! Uint63.lor_spec. rewrite bit_lsl. rewrite! bit_lsl. rewrite bit_1. rewrite! bit_lsr. unfold Uint63.digits. repeat elim_if ; intuition try lia. + rewrite bit_not_int by (unfold Uint63.digits ; lia). destruct (bit k (int_of_nat m + 1 + (int_of_nat p - (int_of_nat m + 1)))). lia. lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR