proposition: Lemma mono_le f (Hf : strict_mono f) : forall n, n <= f n.
proof: Proof. induction n. - auto with arith. - apply Nat.le_lt_trans with (f n); auto with arith. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)