Add some NatRepr lemmas

[atomb]

The following two lemmas are now in what4 but might make more sense here.

leqSubPos :: (1 <= m, 1 <= n, n+1 <= m) => NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
leqSubPos mr nr =
  case (plusComm nr one, plusMinusCancel one nr) of
    (Refl, Refl) ->
      leqSub2 (leqProof (nr `addNat` one) mr) (leqProof nr nr)
  where one = knownNat :: NatRepr 1

leqSuccLeft :: (n + 1 <= m) => p m -> NatRepr n -> LeqProof n m
leqSuccLeft mr nr =
  case (plusComm nr one, addPrefixIsLeq nr one) of
    (Refl, LeqProof) ->
      leqTrans (addIsLeq nr one) (leqProof (nr `addNat` one) mr)
  where one = knownNat :: NatRepr 1