proposition: Lemma log2_lt_lin : forall a, 0<a -> log2 a < a.
proof: Proof. intros a Ha. apply (pow_lt_mono_r_iff 2); try order_pos. apply le_lt_trans with a. - now destruct (log2_spec a Ha). - apply pow_gt_lin_r; order'. Qed.
imports: NZAxioms NZMulOrder NZPow