Derive 1 <= Max a b when (1 <= a ) or (1 <= b)

[lmbollen]

I'm not sure of this is possible, but it's trival that 1 < = Max a b holds when 1 <= a holds or 1 <= b holds.
However, the plugin can't deduce this.

[rowanG077]

Yes and unfortunately it's not super easy to add. Most reasoning this plugin does is local only. So stuff like using other constraints to solve constraints isn't done.

So instead I solve constraints like this using basic axioms:

maxAxiomL
  :: forall (n :: Nat) (p :: Nat) (q :: Nat)
   . (n <= p) :- (n <= Max p q)
maxAxiomL = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))

and a similar one can be defined for the other case.