proposition: Lemma mono_weak f (H: strict_mono f) : forall n p, n <= p -> f n <= f p.
proof: Proof. induction 1. - left. - apply PeanoNat.Nat.lt_le_incl; apply H; auto with arith. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)