Grace/Cumulus/Nat.g17

Open in Workbench Download source

Imports

Pow · Subtraction · Division · Order · Least · Parity · Induction · OrderLemmas · MinMax · PowLemmas · ParityLemmas · CyclicShift

Declarations

Source

1-- Natural-number mathematics2-- 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 Grace.Cumulus.Nat8import Pow9import Subtraction10import Division11import Order12import Least13import Parity14import Induction15import OrderLemmas16import MinMax17import PowLemmas18import ParityLemmas19import CyclicShift20