proposition: Lemma log2_eq_succ_iff_pow2 : forall a, 0<a -> (log2 (S a) == S (log2 a) <-> exists b, S a == 2^b).
proof: Proof. intros a Ha. split. - apply log2_eq_succ_is_pow2. - intros (b,Hb). assert (Hb' : 0 < b). + apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono. + rewrite Hb, log2_pow2; try order'. setoid_replace a with (P (2^b)). * rewrite log2_pred_pow2; trivial. symmetry; now apply lt_succ_pred with 0. * apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0. rewrite <- Hb, lt_succ_r; order. Qed.
imports: NZAxioms NZMulOrder NZPow