proposition: Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).
proof: Proof. destruct n as [|[p|p|]]; discriminate || intros _; simpl; split. - apply (size_le (pos p)). - apply Pos.size_gt. - apply Pos.size_le. - apply Pos.size_gt. - discriminate. - reflexivity. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties