What is the best souce of documentation?

Stream: lean4

[kvanvels]

I am a newbie trying to implement a bunch of statements about the natural numbers (basically the natural numbers game in lean4) I am trying to prove very simple things like for all natural numbers a, a < a + 1, which is easy enough. I want to state and prove a trivial corollary that for all natural number a, a+ 1 > a. Where can I look to start figuring out these questions for myself? Is it best to look at the source code? Maybe in the Ord collection?

For completeness, this is what I need to figure out,

namespace myNamespace
inductive ℕ where
  | zero : ℕ
  | succ : ℕ → ℕ
  deriving Repr

def add (m n : ℕ) : ℕ :=
  match n with
  | ℕ.zero => m
  | ℕ.succ l => ℕ.succ (add m l)

instance : Add ℕ where
  add := add

open ℕ

def lt (m n : ℕ)  : Prop :=  ∃ l : ℕ,  (m + l = n  ∧ l ≠ zero)
def le (n m : ℕ) : Prop := ∃ l : ℕ, n + l = m

instance : LT ℕ where
   lt := lt

instance : LE ℕ where
  le := le

theorem add_succ {m n : ℕ } : m + n.succ = (m + n).succ := rfl
theorem add_zero {m : ℕ} : m + zero = m := rfl

theorem lt_succ (n : ℕ) : n < succ n := by sorry  --(I have a decent proof here that I want to reuse)

theorem succ_gt (n : ℕ) : succ n > n := by
  suffices h₁ : n < succ n from sorry
    --how can I find out what to put here, I want something like ((a < b) implies (b > a) )
  exact lt_succ n



end myNamespace

I appreciate any ideas and direction.

[Yakov Pechersky]

theorem succ_gt (n : ℕ) : succ n > n := lt_succ n

[Yakov Pechersky]

theorem {X : Type _} [LT X] {a b : X} : a < b ↔ b > a := iff.rfl

[kvanvels]

This is surprising to me. Is it correct to say that this means that lean switches greater-thans to less-thans automatically, and that there is no reason to even have my theorem and proof?

[kvanvels]

thanks for the response. I appreciate it.

[Yakov Pechersky]

afaiu, lean4 is able to interpret the gt-syntax as the lt, and vice versa. They (a < b, b > a) both stand for LT.lt a b.

[kvanvels]

Ok. That is nice. In C++ you have define all the different relations. This way seems to make more sense. Do you dig through the source code to learn something like that?

[Arthur Paulino]

I'm not on my PC, but what does #check 1 > 0 say?

Ugh, nvm, I guess it's going to say Prop

[Kevin Buzzard]

@kvanvels b > a is _definitionally equal_ to a < b, and tactics like refl and exact work up to definitional equality. It's the same reason as why m + zero = m is proved by rfl (but of course zero + m = m is not rfl; definitional equality is "not mathematical" in some sense.)