proposition: Lemma smono_Sle f : f 0 <> 0 -> strict_mono f -> S <<= f.
proof: Proof. intros H H0 x; induction x. - destruct (f 0). + now destruct H. + auto with arith. - apply Nat.le_lt_trans with (f x). + auto. + apply H0; auto with arith. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)