fact: Fixpoint find_lowest (n: nat) (k: int) (p: nat) := match p with | O => n | S q => if testbit k (n - p)%nat then (n - p)%nat else find_lowest n k q end.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR