Submission Details

Back to Submissions List

Challenge: solveSub

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:06:06

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 rw [solveSub]; ring

Status: Correct

Feedback: