proposition: Lemma max_mem n0 (s : seq nat) : n0 \in s -> \max_(i <- s) i \in s.
proof: Proof. case: s => // a s _. rewrite big_cons big_seq. elim/big_ind : _ => [|n m|n A]; first exact: mem_head. - rewrite -{5}[a]maxnn maxnACA => ? ?. rewrite {1}/maxn. by case: ifP. - rewrite /maxn. case: ifP; by rewrite ?mem_head // inE A orbT. Qed.
imports: mathcomp(all_ssreflect)