proposition: Lemma log2_up_lt_lin : forall a, 0<a -> log2_up a < a.
proof: Proof. intros a Ha. assert (H : S (P a) == a) by (now apply lt_succ_pred with 0). rewrite <- H at 2. apply lt_succ_r. apply log2_up_le_pow2; trivial. rewrite <- H at 1. apply le_succ_l. apply pow_gt_lin_r. - order'. - apply lt_succ_r; order. Qed.
imports: NZAxioms NZMulOrder NZPow