DEFINITION r_minus()
TYPE =
       ∀i:nat
         .∀n:nat
           .lt n i
             →∀k:K.(eq nat (minus (r k i) (S n)) (r k (minus i (S n))))
BODY =
Show proof