proposition: Lemma log2_spec_alt : forall a, 0<a -> exists r, a == 2^(log2 a) + r /\ 0 <= r < 2^(log2 a).
proof: Proof. intros a Ha. destruct (log2_spec _ Ha) as (LE,LT). destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). exists r. split. - now rewrite add_comm. - split. + trivial. + apply (add_lt_mono_r _ _ (2^log2 a)). rewrite <- Hr. generalize LT. rewrite pow_succ_r by order_pos. rewrite two_succ at 1. now nzsimpl. Qed.
imports: NZAxioms NZMulOrder NZPow