proposition: Lemma find_lowest_spec: forall n p k, testbit k n = true -> (forall q, ((n - p)%nat <= q < find_lowest n k p)%nat -> testbit k q = false) /\ testbit k (find_lowest n k p) = true.
proof: Proof. induction p; intros. - simpl. split; auto. intros; lia. - exploit IHp; eauto. intros [HA HB]. simpl. case_eq (testbit k (n - S p)%nat); intros. + split; intros; auto; lia. + split; intros; auto. destruct (Nat.eq_dec (n - S p)%nat q). * subst q. auto. * apply HA; lia. Qed.
imports: Lia Cdcl.Coqlib