ssreflect中如何对maxr表达式进行分情况分析？

ssreflect配合MathComp库原生支持对maxr表达式做分情况讨论，不需要额外编写自定义策略，有两种常用实现方式：

• 使用maxr预置的专用分情况引理（推荐）
  MathComp库中针对实数最大值函数maxr已经内置了分情况析取引理，直接调用即可自动完成分支拆分和目标重写：

  have [h_x0_is_max | h_x_is_max] := maxr_cases x0 x.
  

  第一个分支会自动得到x <= x0的前提，同时目标中所有maxr x0 x会被重写为x0，对应x0为最大值的场景；第二个分支会自动得到x0 <= x的前提，同时目标中所有maxr x0 x会被重写为x，对应x为最大值的场景。
• 复用ifP写法
  maxr本身的底层定义就是基于大小比较的if表达式，你可以先展开maxr的定义再调用ifP做拆分：

  rewrite /maxr; have [h_ge | h_lt] := ifP.
  

  第一个分支会得到x0 >= x成立的前提，对应maxr x0 x = x0；第二个分支会得到~(x0 >= x)（即x > x0）成立的前提，对应maxr x0 x = x。这种方式需要你后续手动重写目标中的maxr表达式，不如专用引理便捷。

注意：如果你的环境中找不到maxr_cases引理，可以先检查是否正确导入了ssreflect的实数相关库，具体导入语句取决于你使用的MathComp版本。

内容的提问来源于stack exchange，提问作者dvr