Radosław Rowicki
Prowadził warsztaty:
- WWW13 (2017): Programowanie Funkcyjne
- WWW15 (2019): Programowanie Funkcyjne
- WWW16 (2020): Rachunek Lambda, Typy i Logika Intuicjonistyczna
- WWW17 (2021): Programowanie w Logice Odwołane
- WWW17 (2021): Programowanie od podstaw
- WWW20 (2024): Programowanie dowodami
Niniejszym przedstawiam dowód, iż 1 jest największą liczbą naturalną:
Niech n będzie największą liczbą naturalną.
n2 ≤ n (z założenia)
n2 - n ≤ 0
n(n - 1) ≤ 0
n ≥ 0 ∧ n ≤ 1
n = 0 ∨ n = 1 (bo n naturalne)
n = 1, bo 1 > 0, a n ma być przecież największe
CND.