proposition: Lemma mono_injective f (Hf : strict_mono f) : forall n p , f n = f p -> n = p.
proof: Proof. intros n p H; destruct (PeanoNat.Nat.lt_total n p). - specialize (Hf _ _ H0); rewrite H in Hf; destruct (Nat.lt_irrefl _ Hf). - destruct H0; trivial. + specialize (Hf _ _ H0); rewrite H in Hf; destruct (Nat.lt_irrefl _ Hf). Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)