proposition: Lemma log2_log2_up_exact : forall a, 0<a -> (log2 a == log2_up a <-> exists b, a == 2^b).
proof: Proof. intros a Ha. split. - intros H. exists (log2 a). generalize (log2_log2_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b,Hb). rewrite Hb. destruct (le_gt_cases 0 b). + now rewrite log2_pow2, log2_up_pow2. + rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos. Qed.
imports: NZAxioms NZMulOrder NZPow