fact: Fixpoint Pos_log2floor_plus1 (p : positive) : positive := match p with | (p'~1)%positive => Pos.succ (Pos_log2floor_plus1 p') | (p'~0)%positive => Pos.succ (Pos_log2floor_plus1 p') | 1%positive => 1 end.
imports: QArith Qpower Qabs Qround Lia Lqa PosExtra