proposition: Theorem lognat_ge_monotonic_b : forall(a : nat)(pf1 : (a <> 0))(pf2: (S a) <> 0), (lognat pf2) >= (lognat pf1).
proof: Proof. induction a. intros. destruct pf1. auto. intros. unfold lognat in *. rewrite (factor_s_conv pf1). apply log2_monotonic_b. Qed.
imports: ZArith micromega.Lia