proposition: Lemma max_homo : {homo f : x y / (x <= y)%O >-> (x <= y)%O} -> {morph f : x y / max x y}.
proof: Proof. (move=> fH x y; case: (leP (f x)) => [fxLfy|fyLfx]; case: leP => //). by rewrite lt_neqAle => /andP[_ /fH]; case: ltgtP fxLfy. by move=> /fH; case: ltgtP fyLfx. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)