proposition: Lemma comparable_maxr z : {in >=<%O z &, forall x y, z >=< max x y}.
proof: Proof. by move=> x y cmp_xz cmp_yz; rewrite /max; case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)