proposition: Lemma max_lub_l_ssr n m p: max n m < p -> n < 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)