theorem not_lt_self_demo (n : Nat) : ¬ n < n := Nat.lt_irrefl n