proposition: Lemma log2_pos : forall a, 1<a -> 0 < log2 a.
proof: Proof. intros a Ha. assert (Ha' : 0 < a) by order'. assert (H := log2_nonneg a). le_elim H; trivial. generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order. intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order. Qed.
imports: NZAxioms NZMulOrder NZPow