avigad

import Init

/- Facts about Nat -/

theorem Nat.le_refl (a : Nat) : a ≤ a := sorry
theorem Nat.le_trans {a b c : Nat} : a ≤ b → b ≤ c → a ≤ c := sorry
theorem Nat.lt_trans {a b c : Nat} : a < b → b < c → a < c := sorry
theorem Nat.le_of_lt {a b : Nat} : a < b → a ≤ b := sorry
theorem Nat.not_le_of_lt {a b : Nat} : a < b → ¬ b ≤ a := sorry
theorem Nat.le_of_not_le {a b : Nat} : ¬ a ≤ b → b ≤ a := sorry

avigad

/-
Notes on dependent type theory and Lean's formal foundation
Jeremy Avigad
Hausdorff School: Formal Mathematics and Computer-Assisted Proving
September 18 - 22, 2023
https://tinyurl.com/bonn-dtt
-/

import Mathlib.Data.Real.Basic
import Mathlib.Data.Matrix.Basic