proposition: Lemma max_lub_ssr n m p : n < p -> m < p -> max n m < p.
proof: Proof. move => /ltP H1 /ltP H2. apply/ltP/PeanoNat.Nat.max_lub_lt; eassumption. Qed.
imports: List ZArith Tactics mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq)