let inv (t:t) : bool = snd t >= fst t

Forall i:int, inv (singleton i) = true
       inv (singleton i)          LHS
       inv (i,i)                  eval singleton
       snd (i,i) >= fst (i,i)     eval inv
       i >= i                     eval snd, fst
       true                       reflexive property of equality and
                                  law of trichotomy
                                

Forall i:int, j:int, inv (range i j) = true
       inv (range i j)            LHS
       inv (min i j, max i j)     eval range
       max i j >= min i j         eval inv
       true                       definition of max, min


Forall x:t, i:int, inv x -> inv (x+i)
IMS: Assume inv x, inv (x+i) = true
       inv (x+i)                  LHS
       inv ((fst x)+i,(snd x)+i)  eval (+)
       snd ((fst x)+i,(snd x)+i)>=
       fst ((fst x)+i,(snd x)+i)  eval inv
       (snd x)+i >= (fst x)+i     eval snd, fst
       snd x >= fst x             additive property of inequality
       inv x                      reverse eval inv
       true                       premise inv x
       

Forall x:t, i:int, inv x -> inv (x*i)
IMS: Assume inv x, inv (x*i) = true

Case i < 0:
       inv (x*i)                  LHS
       inv ((snd x)*i,(fst x)*i)  eval (*)
       snd ((snd x)*i,(fst x)*i)>=
       fst ((snd x)*i,(fst x)*i)  eval inv
       (fst x)*i >= (snd x)*i     eval snd, fst
       fst x <= snd x             multiplicative property of inequality
       snd x >= fst x             converse of <= and >=
       inv x                      reverse eval inv
       true                       premise inv x


Case i >= 0:
       inv (x*i)                  LHS
       inv ((fst x)*i,(snd x)*i)  eval (*)
       snd ((fst x)*i,(snd x)*i)>=
       fst ((fst x)*i,(snd x)*i)  eval inv
       (snd x)*i >= (fst x)*i     eval snd, fst
       snd x >= fst x             multiplicative property of inequality
       inv x                      reverse eval inv
       true                       premise inv x

Forall x:t, y:t, (inv x) && (inv y) -> inv (bridge x y)
IMS: Assume inv x and inv y, inv (bridge x y) = true
1       inv (bridge x y)           LHS
2       inv (min (fst x) (fst y),
             max (snd x) (snd y))  eval bridge
3       snd (min (fst x) (fst y),
             max (snd x) (snd y))>=
        fst (min (fst x) (fst y),
             max (snd x) (snd y))  eval inv
4       max (snd x) (snd y) >=
        min (fst x) (fst y)        eval snd, fst

At this point we will break into 4 cases.
Case snd x >= snd y, fst y >= fst x
5      snd x >= fst x              case definition
6      inv x                       reverse eval inv
7      true                        premise inv x
      
Case snd x >= snd y, fst x >= fst y
5      snd x >= fst y              case definition
6      true                        transitive property of inequality
                                   for case definition and premise inv y

Case snd y >= snd x, fst y >= fst x
5      snd y >= fst x              case definition
6      true                        transitive property of inequality
                                   for case definition and premise inv x

Case snd y >= snd x, fst x >= fst y
5      snd y >= fst y              case definition
6      inv y                       reverse eval inv
7      true                        premise inv y

(
 NB1: it would be easier, and perhaps reasonable, but much less explicit,
     to just use this step instead of a case-wise approach:
     true                       transitivity of inequality, premises
)

NB2: we don't have to prove anything about size, contains, or (<),
because they don't produce a range.