proposition: Lemma log2_up_eq_succ_is_pow2 : forall a, log2_up (S a) == S (log2_up a) -> exists b, a == 2^b.
proof: Proof. intros a H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite 2 (proj2 (log2_up_null _)) in H. + generalize (lt_succ_diag_r 0); order. + order'. + apply le_succ_l. order'. - assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono). exists (log2_up a). generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)). rewrite H, pred_succ, lt_succ_r. order. Qed.
imports: NZAxioms NZMulOrder NZPow