proposition: Lemma log2_up_same : forall a b, 0<a -> 0<b -> log2_up a == log2_up b -> a < 2*b.
proof: Proof. intros a b Ha Hb H. apply log2_up_lt_cancel. rewrite log2_up_double, H by trivial. apply lt_succ_diag_r. Qed.
imports: NZAxioms NZMulOrder NZPow