recall: let LHPR.inv = (lo <= hi)
and consider: let LLPR.inv = (len > 0)

let abs (llpr:LoLenPairRange.t) (lhpr:LoHiPairRange.t) =
    let (lo, len) = llpr in
    (lo, lo+len-1) = lhpr

Forall k:int:
       abs (L.singleton k) (H.singleton k) = true

Pick an arbitrary k.
abs (L.singleton k) (H.singleton k)             LHS
abs (k,1) (k,k)                                 eval x2
(k,k+1-1) = (k,k)                               eval abs
(k,k) = (k,k)                                   math
true                                            reflexivity

Forall i,j:int:
       abs (L.range i j) (H.range i j) = true

Pick an arbitrary i, j.
abs (L.range i j) (H.range i j)                                         LHS
abs ((min i j), (max i j)-(min i j)+1) ((min i j), (max i j))           eval x2
(min i j, (min i j)+((max i j)-(min i j)+1)-1) = ((min i j), (max i j)) eval abs
(min i j, max i j) = (min i j, max i j)                                 math
true                                                                    reflexivity

Forall l:(int list), p:(int*int), k:int:
       if (L.inv l) and (H.inv p) and (abs l p) then
       abs (L.(+) l k) (H.(+) p k) = true

Forall l:(int list), p:(int*int), k:int:
       if (L.inv l) and (H.inv p) and (abs l p) then
       abs (L.(*) l k) (H.(*) p k) = true

Forall l1,l2:(int list), p1,p2:(int*int): 
       if (L.inv l1) and (L.inv l2) and (H.inv p1) and (H.inv p2)
          and (abs l1 p1) and (abs l2 p2) then
       (abs (L.bridge l1 l2) (H.bridge p1 p2)) = true

Forall l:(int list), p:(int*int):
       if (L.inv l) and (H.inv p) and (abs l p) then
       L.size l = H.size p

Forall l:(int list), p:(int*int), k:int:
	if (L.inv l) and (H.inv p) and (abs l p) then
        L.contains l k = H.contains p k

Forall l1,l2:(int list), p1,p2:(int*int): 
	if (L.inv l1) and (L.inv l2) and (H.inv p1) and (H.inv p2)
           and (abs l1 p1) and (abs l2 p2) then
	     L.(<) l1 l2 = None and H.(<) p1 p2 = None 
	      OR
	     L.(<) l1 l2 = Some b and H.(<) p1 p2 = Some b' and b=b'.