proposition: Lemma log2_null : forall a, log2 a == 0 <-> a <= 1.
proof: Proof. intros a. split; intros H. - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. generalize (log2_pos a Ha); order. - le_elim H. + apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. + rewrite H. apply log2_1. Qed.
imports: NZAxioms NZMulOrder NZPow