proposition: Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).
proof: Proof. assert (Pow : forall p q, pos (p^q) = (pos p)^(pos q)). { intros. now apply Pos.iter_swap_gen. } destruct n as [|[p|p|]|]; intros Hn; split; try easy; unfold log2; simpl succ; rewrite ?Pos.add_1_r, <- Pow. - change (2^Pos.size p <= Pos.succ (p~0))%positive. apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le. - apply Pos.size_gt. - apply Pos.size_le. - apply Pos.size_gt. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass