RealLinearErgo

Checked real-order linarith examples

Open in Workbench View on GitHub

1-- Checked real-order linarith examples2-- 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 RealLinearErgo8import Grace.Cumulus.Real.Analysis.HeineCantor910theorem add_bounds (x y u v : Real)11  requires first : x < y12  requires second : u < v13  shows x + u < y + v14proof15  linarith1617theorem mixed_bounds (x y z : Real)18  requires first : x ≤ y19  requires second : y < z20  shows x < z21proof22  linarith23