proposition: Theorem lowest_bit_spec: forall k, k <> zero -> exists n, is_mask (lowest_bit k) n /\ (forall p, (p < n)%nat -> testbit k p = false).
proof: Proof. intros. unfold lowest_bit. destruct (K.LPO k H) as [n H0]. { generalize (find_lowest_spec n n k H0). intros [HA HB]. assert (HC: forall p, (p < find_lowest n k n)%nat -> testbit k p = false) by (intros; apply HA; lia). generalize (lopp_spec_low _ _ HC HB). intros HD. generalize (lopp_spec_eq _ _ HC HB). intros HE. generalize (lopp_spec_high _ _ HC HB). intros HF. exists (find_lowest n k n). intros; split; intros. { intros; split; intros. - rewrite land_spec in H1. apply andb_true_iff in H1; destruct H1. unfold lopp in H2. destruct (lt_dec p (find_lowest n k n)). + rewrite HD in H2; auto. congruence. + destruct (gt_dec p (find_lowest n k n)). * rewrite HF in H2; auto. rewrite H1 in H2. simpl in H2. congruence. * lia. - subst. rewrite land_spec. apply andb_true_iff. split. + unfold testbit in HB. auto. + unfold lopp. auto. } { apply HC; auto. } } Qed.
imports: Lia Cdcl.Coqlib