LeastNaturalStarter

Least-number selection is available from the Nat import, in ZF

Open in Workbench View on GitHub

1-- Least-number selection is available from the Nat import, in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module LeastNaturalStarter8import Grace.Cumulus.Nat9import Grace.Cumulus.Set.Core1011theorem least_of_unordered_pair12  shows leastNatural({7, 3}) = 313proof14  have three : Nat(3) by typecheck15  have seven : Nat(7) by typecheck16  have inhabited : Nonempty({7, 3})17    unfold Nonempty18    witness 319    exact pair.right20  have naturals : {7, 3} ⊆ ℕ21    have threeIn := nat.omega.forward with three22    have sevenIn := nat.omega.forward with seven23    simp24  have selected := leastNatural.selected at {7, 3} with *25  rcases selected with ⟨natural, member, minimal⟩26  have chosenNat := nat.omega.backward with natural27  have threeMember := pair.right at 7, 328  have bound := leastNatural.least at {7, 3}, 3 with *29  have alternatives := pair.membership.forward at 7, 3, leastNatural({7, 3}) with member30  cases alternatives with isSeven | isThree31  . rw isSeven at bound32    have impossible : 7 < 7 by arith33    exfalso34    exact Less.irreflexive with seven, impossible35  . exact isThree36