Reasoning about Integers

Stream: lean4

[Aymeric Fromherz]

Hi,
I'm trying to do small arithmetic proofs with Lean 4, and I'm struggling with the following small lemma
def foo (x : Nat) : 0 <= Int.ofNat x := by sorry

I found Nat.zero_le which almost gives me what I need, but I still need to prove that x <= y -> Int.ofNat x <= Int.ofNat y
Is this lemma somewhere in the standard library (and what is the recommended way to look for such lemmas, and/or to do proofs on integers)?
Thanks!

[Marcus Rossel]

Here's a proof:

def foo (x : Nat) : 0 <= Int.ofNat x := Int.NonNeg.mk _

[Aymeric Fromherz]

Thanks!

[Marcus Rossel]

The <= notation corresponds to LE.le. The LE instance for Int uses Int.le:

protected def Int.le (a b : Int) : Prop := NonNeg (b - a)

where

inductive NonNeg : Int → Prop where
  | mk (n : Nat) : NonNeg (ofNat n)

So if you want to prove (x <= y) → (Int.ofNat x <= Int.ofNat y) you could start like this:

example : (x <= y) → (Int.ofNat x <= Int.ofNat y) := by
  intro h
  simp [LE.le, Int.le]

which then requires you to prove:

⊢ Int.NonNeg (Int.ofNat y - Int.ofNat x)