Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: Kevin Buzzard

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

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:= -a

First Theorem Proof:

theorem solveAdd0_correct(a: Int): a +(solveAdd0 a)=0

:= by
  unfold solveAdd0
  exact?

Status: Correct

Feedback:

Try this: exact Int.add_right_neg a