proposition: Lemma mono_f_gt_0 f : mono f -> 0 < f 0 -> f_gt_from 0 f.
proof: Proof. intros H H0 i _. induction i. assumption. apply Nat.le_lt_trans with (f i). unfold id_nat; auto with arith. apply H. auto with arith. Qed.
imports: Coq(ArithRing Lia Arith)