rewrite_error.idr

-- as long as there is a proof that a < b then we can build a Fin b
natToProvedFin : (n : Nat) -> (bound : Nat) -> {auto prf : LT n bound} -> Fin bound
natToProvedFin Z (S right) {prf=LTESucc x} = FZ
natToProvedFin (S k) (S right) {prf=LTESucc x} = FS $ natToProvedFin k right

record Numbers where
  constructor MkNumbers
  max : Nat
  bonus : Nat
  current : Fin (S (max + bonus))

setMaxCurr : Nat -> Numbers -> Numbers
setMaxCurr newMax (MkNumbers max bonus current) with (cmp newMax max)
  -- newMax lower, therefore, lower current
  setMaxCurr newMax (MkNumbers (newMax + (S y)) bonus current) | (CmpLT y) =
    ?setMaxCurr_rhs_1
    --newMax Equal, update current
  setMaxCurr max (MkNumbers max bonus current) | CmpEQ =
    rewrite plusZeroRightNeutral max in -- if we remove rewrite Idris cannot find the proof
            MkNumbers max bonus (natToProvedFin max (S (max + 0)))
  -- newMax higher, set as bonus and update current
  setMaxCurr (max + (S x)) (MkNumbers max bonus current) | (CmpGT x) = ?setMaxCurr_rhs_3