proposition: Lemma max_lub_r_ssr n m p: max n m < p -> m < p.
proof: Proof. move /ltP/PeanoNat.Nat.max_lub_lt_iff => [_ /ltP H1]. assumption. Qed.
imports: List ZArith Tactics mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq)