proposition: Lemma log2_up_null : forall a, log2_up a == 0 <-> a <= 1.
proof: Proof. intros a. split; intros H. - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. generalize (log2_up_pos a Ha); order. - now apply log2_up_eqn0. Qed.
imports: NZAxioms NZMulOrder NZPow