proposition: Lemma log2_succ_double : forall a, 0<a -> log2 (2*a+1) == S (log2 a).
proof: Proof. intros a Ha. rewrite add_1_r. destruct (log2_succ_or (2*a)) as [H|H]; [exfalso|now rewrite H, log2_double]. apply log2_eq_succ_is_pow2 in H. destruct H as (b,H). destruct (lt_trichotomy b 0) as [LT|[EQ|LT]]. - rewrite pow_neg_r in H; trivial. apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. rewrite <- one_succ in Ha. order'. - rewrite EQ, pow_0_r in H. apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. rewrite <- one_succ in Ha. order'. - assert (EQ:=lt_succ_pred 0 b LT). rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ]. destruct (lt_ge_cases a (2^(P b))) as [LT'|LE']. + generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order. + rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'. rewrite <- H in LE'. apply le_succ_l in LE'. order. Qed.
imports: NZAxioms NZMulOrder NZPow