Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: Kevin Buzzard

Submitted at: 2024-11-15 11:36:14

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

:= b - a

First Theorem Proof:

theorem solveAdd_correct (a b: Int): a + (solveAdd a b) =b 

:= by 
  unfold solveAdd
  exact?

Status: Correct

Feedback:

Try this: exact add_sub_cancel'_right a b