Case analysis on max - ssreflect

Question

I have the following in my goal:

maxr x0 x

I would like to do a case analysis, to consider what happens in the case that x0 is greatest, and the case the x is greatest. Is this possible in ssreflect?

Generally it would be something like (for example with if statement)

have [ something | something'] := ifP

However, I cannot find the appropriate syntax to do a case analysis with max.

Answer 1

You can use lerP or ltrP:

Check lerP.
(*
lerP
     : forall (R : realDomainType) (x y : R),
       ler_xor_gt (R:=R) x y (minr y x) (minr x y) 
         (maxr y x) (maxr x y) `|(x - y)%R| `|(y - x)%R| 
         (x <= y)%R (y < x)%R
*)

In action:

From mathcomp Require Import all_ssreflect all_algebra.
Import Num.Def Num.Theory.

Goal forall a b : int, maxr a b = a.
  move=> a b.
  case: lerP.
(*
2 goals (ID 4070)
  
  a, b : int
  ============================
  (a <= b)%R -> b = a

goal 2 (ID 4071) is:
 (b < a)%R -> a = a
*)
Abort.

I found them with Search maxr., which is not the fastest way (it shows several results), but at least it works.