IntegerRingStarter

Part of Cumulus, the Grace17 mathematics library

Open in Workbench View on GitHub

1-- Part of Cumulus, the Grace17 mathematics library.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module IntegerRingStarter7import Grace.Cumulus.Int89theorem signed_product (x y : Integer)10  shows (-x) * (-y) = x * y11proof12  ring1314theorem difference_of_squares (x y : Integer)15  shows (x + y) * (x - y) = x * x - y * y16proof17  ring1819theorem cancellation (x y : Integer)20  shows (x + y) + (-y) = x21proof22  ring2324theorem units (x : Integer)25  shows x * 1 + 0 = x26proof27  ring2829theorem cubic (x y : Integer)30  shows (x - y) * (x * x + x * y + y * y) = x * x * x - y * y * y31proof32  ring33