
  0 | ||| Special subtraction of a `Fin` from a `Nat`
  1 | module Data.Fin.Minus
  2 | 
  3 | import public Data.Fin
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | (-) : (n : Nat) -> Fin (S n) -> Nat
  9 | n   - FZ   = n
 10 | S k - FS x = k - x
 11 | 
 12 | export
 13 | plus_discards_minus : (n : Nat) -> (f : Fin $ S n) -> (n - f) + finToNat f = n
 14 | plus_discards_minus k     FZ     = rewrite plusZeroRightNeutral k in Refl
 15 | plus_discards_minus (S k) (FS x) = rewrite sym $ plusSuccRightSucc (k - x) (finToNat x) in
 16 |                                    rewrite plus_discards_minus k x in
 17 |                                    Refl
 18 | 
 19 | export
 20 | minus_last_gives_0 : (n : Nat) -> n - Fin.last = 0
 21 | minus_last_gives_0 Z     = Refl
 22 | minus_last_gives_0 (S k) = minus_last_gives_0 k
 23 |