proposition: Lemma LPO : forall (k:Uint63.int), k <> zero -> exists p, testbit k p = true.
proof: Proof. intros. unfold zero in *. assert (LPO: (exists p, ((p <? int_of_nat size) = true) /\ (bit k p = true))%uint63). { case (to_Z_bounded k). unfold wB. assert (0 < size <= 63). { unfold size. lia. } revert k H. induction size; try lia. intros. assert (n = 0 \/ 0 < n) by lia. destruct H3. - subst. assert (k = one). { change (2 ^Z.of_nat 1)%Z with 2%Z in H2. unfold one. lia. } subst. exists 0%uint63. split. unfold int_of_nat. lia. apply bit_1. - assert ((k >> 1) = 0 \/ (k >> 1) <> 0)%uint63 by lia. destruct H4. + exists 0%uint63. unfold int_of_nat. split. lia. destruct (bit k 0) eqn:B0;auto. rewrite (bit_split k) in H. rewrite B0 in H. rewrite H4 in H. compute in H. lia. + assert (exists p : int, (p <? int_of_nat n)%uint63 = true /\ bit (k >> 1) p = true). { apply IHn ; auto. lia. lia. rewrite lsr_spec. replace (Z.of_nat (S n)) with (1 + Z.of_nat n)%Z in H2 by lia. rewrite Z.pow_add_r in H2 by lia. lia. } destruct H5. exists (x+1)%uint63. split. unfold int_of_nat in *. lia. destruct H5. rewrite bit_lsr in H6. destruct ((x ≤? 1 + x)%uint63) eqn:EQ ; try lia. rewrite <- H6. f_equal. lia. } destruct LPO. exists (Z.to_nat (to_Z x)). unfold testbit. destruct (63 <=? Z.to_nat (to_Z x)) eqn:LE. unfold int_of_nat,size in H0. lia. destruct H0. rewrite <- H1. f_equal. unfold int_of_nat; lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR