proposition: Lemma log2_nonneg : forall a, 0 <= log2 a.
proof: Proof. intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite log2_nonpos. - destruct (log2_spec a Ha) as (_,LT). apply lt_succ_r, (pow_gt_1 2). + order'. + rewrite <- le_succ_l, <- one_succ in Ha. order. Qed.
imports: NZAxioms NZMulOrder NZPow