Decompose Max/MinInterval to avoid CHOOSE in one-liner BY

THEOREM MaxInterval and THEOREM MinInterval in
FiniteSetsExtTheorems_proofs were both discharged by a single

  BY DEF Max     (resp. BY DEF Min)

After unfolding, the obligation contains the raw CHOOSE that defines
Max/Min, e.g.

  (CHOOSE x \in a..b : \A y \in a..b : x >= y) = b

To close that in one shot, a backend has to reason about CHOOSE
uniqueness while simultaneously doing arithmetic on the interval a..b.
Zenon has very limited support for CHOOSE and reported "exhausted search
space" with the macOS arm64 build of TLAPS 1.6.0-pre, while another
bundled prover happened to find the proof on Linux.  Either way, relying
on a CHOOSE-savvy backend for these two facts is fragile across tlapm
builds.

Rewrite both proofs to go through the existing MaxInt / MinInt
introduction rules of the same module, which already hide the CHOOSE
behind

  ASSUME S \in SUBSET Int, x \in S, \A y \in S : x >= y
  PROVE  Max(S) = x

interface.  Each new proof supplies the two trivial arithmetic side
conditions (b \in a..b and \A y \in a..b : b >= y, and the symmetric
pair for Min) so that no backend ever sees the CHOOSE.

All 419 obligations of FiniteSetsExtTheorems_proofs continue to check
locally with `tlapm --cleanfp`.

[Proofs]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

modules/FiniteSetsExtTheorems_proofs.tla

@@ -550,7 +550,11 @@ THEOREM MaxIntBounded ==
 THEOREM MaxInterval ==
     ASSUME NEW a \in Int, NEW b \in Int, a <= b 
     PROVE  Max(a..b) = b
-BY DEF Max
+<1>1. b \in a..b
+  OBVIOUS
+<1>2. \A y \in a..b : b >= y
+  OBVIOUS
+<1>. QED  BY <1>1, <1>2, MaxInt
 
 THEOREM MinInt ==
     ASSUME NEW S \in SUBSET Int, NEW x \in S, \A y \in S : x <= y
@@ -605,7 +609,11 @@ THEOREM MinIntBounded ==
 THEOREM MinInterval ==
     ASSUME NEW a \in Int, NEW b \in Int, a <= b 
     PROVE  Min(a..b) = a
-BY DEF Min 
+<1>1. a \in a..b
+  OBVIOUS
+<1>2. \A y \in a..b : a <= y
+  OBVIOUS
+<1>. QED  BY <1>1, <1>2, MinInt
 
 THEOREM MinNat ==
     ASSUME NEW S \in SUBSET Nat, S # {}