proposition: Lemma log2_succ_le : forall a, log2 (S a) <= S (log2 a).
proof: Proof. intros a. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. - apply (pow_le_mono_r_iff 2); try order_pos. transitivity (S a). + apply log2_spec. apply lt_succ_r; order. + now apply le_succ_l, log2_spec. - rewrite <- EQ, <- one_succ, log2_1; order_pos. - rewrite 2 log2_nonpos. + order_pos. + order'. + now rewrite le_succ_l. Qed.
imports: NZAxioms NZMulOrder NZPow