proposition: Lemma log2_eq_succ_is_pow2 : forall a, log2 (S a) == S (log2 a) -> exists b, S a == 2^b.
proof: Proof. intros a H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite 2 (proj2 (log2_null _)) in H. + generalize (lt_succ_diag_r 0); order. + order'. + apply le_succ_l. order'. - assert (Ha' : 0 < S a) by (apply lt_succ_r; order). exists (log2 (S a)). generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)). rewrite <- le_succ_l, <- H. order. Qed.
imports: NZAxioms NZMulOrder NZPow