Introduction

First steps with sets, theorem application, and integer algebra

Open in Workbench View on GitHub

1-- First steps with sets, theorem application, and integer algebra.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 Introduction8import Grace.Cumulus.Set.Core9import Grace.Cumulus.Int1011theorem subset_step (A B x : Set)12  requires included : A ⊆ B13  requires member : x ∈ A14  shows x ∈ B15proof16  simp1718theorem subset_chain (A B C : Set)19  requires first : A ⊆ B20  requires second : B ⊆ C21  shows A ⊆ C22proof23  exact Subset.transitive with *2425theorem difference_of_squares (x y : Integer)26  shows (x + y) * (x - y) = x * x - y * y27proof28  ring29