Submission Details

Back to Submissions List

Challenge: solveSub

Submitted by: kvanvels

Submitted at: 2024-11-15 17:06:53

Code:

import Init.Data.Int

def solveSub(a b:Int): Int

:= a - b

First Theorem Proof:

theorem solveSub_correct(a b:Int): a - (solveSub a b)=b

:= by
  unfold solveSub
  exact
    calc a - (a-b) = (a - a) + b := by rw [sub_add a a b]
                 _ = 0 + b       := by rw [sub_self]
                 _ = b           := by rw [zero_add]

  

Status: Correct

Feedback: