Grace/Cumulus/Real/Addition.g17

Open in Workbench Download source

Imports

Embedding

Declarations

Source

1-- Addition of Dedekind real numbers2-- 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.Real.Addition8import Embedding910-- The lower cut generated by all rational sums a+b with a ∈ A and b ∈ B.11-- Writing the strict lower closure into the definition makes downward closure12-- and roundedness consequences of the rational order itself.13def realAddCut (A B : Set) : Set :=14  { q ∈ ℚ |15    ∃ a ∈ A, ∃ b ∈ B,16      relates(rationalLess, q, rationalAdd((a, b))) }1718-- The real zero is the lower rational cut at zero.  Its soft result type lets19-- overloaded real notation recognize it, while realZero.real below supplies20-- the kernel-checked mathematical certificate.21def realZero : Real := rationalCut(rationalZero)2223theorem realZero.real24  shows Real(realZero)25proof26  unfold realZero27  exact rationalCut.real with rationalZero.rational2829instance realZero.of_nat30  shows OfNat(ℝ, 0, realZero)31proof32  constructor33  . typecheck34  . exact realZero.real3536-- Public-facing membership avoids exposing the underlying function-graph37-- application.  The witnesses are still checked against the same definition.38theorem realAddCut.membership_value (A B q : Set)39  shows q ∈ realAddCut(A, B) ↔40    (q ∈ ℚ ∧ ∃ a ∈ A, ∃ b ∈ B,41      q < rationalAddValue(a, b))42proof43  constructor44  . intro member45    obtain ⟨qInQ, a, aInA, b, bInB, less⟩ := realAddCut.membership.forward with member46    refine ⟨qInQ, a, aInA, b, bInB, _⟩47    unfold rationalAddValue48    exact less49  . intro data50    rcases data with ⟨qInQ2, c, cInA, d, dInB, less2⟩51    unfold rationalAddValue at less252    exact realAddCut.membership.backward with ⟨qInQ2, c, cInA, d, dInB, less2⟩5354theorem realAddCut.subset_rationals (A B : Set)55  shows (realAddCut(A, B) ⊆ ℚ)56proof57  simp5859theorem realAddCut.nonempty (A B : Real)60  shows Nonempty(realAddCut(A, B))61proof62  have cutA := Real.characterization.forward at A with assumption63  have cutB := Real.characterization.forward at B with assumption64  obtain ⟨a, aInA⟩ := DedekindCut.nonempty with cutA65  obtain ⟨b, bInB⟩ := DedekindCut.nonempty with cutB66  have subsetA := DedekindCut.subset_rationals with cutA67  have subsetB := DedekindCut.subset_rationals with cutB68  have aInQ := subsetA with a, aInA69  have bInQ := subsetB with b, bInB70  have aRational : Rational(a) by exact aInQ71  have bRational : Rational(b) by exact bInQ72  have sumRational := rationalAddValue.rational_raw with aRational, bRational73  obtain ⟨q, qInQ, qLessSum⟩ := rationalLess.exists_below with sumRational74  witness q75  apply realAddCut.membership.backward76  constructor77  . exact qInQ78  . witness a79    constructor80    . exact aInA81    . witness b82      constructor83      . exact bInB84      . unfold rationalAddValue at qLessSum85        exact qLessSum8687theorem realAddCut.downward (A B p q : Set)88  requires realA : Real(A)89  requires realB : Real(B)90  requires qInSum : q ∈ realAddCut(A, B)91  requires pInQ : p ∈ ℚ92  requires pLessQ : relates(rationalLess, p, q)93  shows p ∈ realAddCut(A, B)94proof95  obtain ⟨qInQ, a, aInA, b, bInB, qLessSum⟩ := realAddCut.membership.forward with qInSum96  have cutA := Real.characterization.forward with realA97  have cutB := Real.characterization.forward with realB98  have subsetA := DedekindCut.subset_rationals with cutA99  have subsetB := DedekindCut.subset_rationals with cutB100  have aRational : Rational(a)101    unfold Rational102    exact subsetA with a, aInA103  have bRational : Rational(b)104    unfold Rational105    exact subsetB with b, bInB106  have transitive := rationalLess.transitive_on107  have sumInQ := rationalAddValue.rational_raw with aRational, bRational108  unfold rationalAddValue at sumInQ109  have pLessSum := transitive with110    p, pInQ, q, qInQ, rationalAdd((a, b)), sumInQ, pLessQ, qLessSum111  exact realAddCut.membership.backward with ⟨pInQ, a, aInA, b, bInB, pLessSum⟩112113theorem realAddCut.no_greatest (A B q : Set)114  requires realA : Real(A)115  requires realB : Real(B)116  requires qInSum : q ∈ realAddCut(A, B)117  shows ∃ r ∈ realAddCut(A, B), relates(rationalLess, q, r)118proof119  obtain ⟨qInQ, a, aInA, b, bInB, qLessSum⟩ := realAddCut.membership.forward with qInSum120  have cutA := Real.characterization.forward with realA121  have cutB := Real.characterization.forward with realB122  have subsetA := DedekindCut.subset_rationals with cutA123  have subsetB := DedekindCut.subset_rationals with cutB124  have aRational : Rational(a)125    unfold Rational126    exact subsetA with a, aInA127  have bRational : Rational(b)128    unfold Rational129    exact subsetB with b, bInB130  have sumRational := rationalAddValue.rational_raw with aRational, bRational131  have qRational : Rational(q) by exact qInQ132  unfold rationalAddValue at sumRational133  obtain ⟨r, rInQ, qLessR, rLessSum⟩ := rationalLess.dense with qRational, sumRational, qLessSum134  witness r135  constructor136  . apply realAddCut.membership.backward at A, B, r137    refine ⟨rInQ, a, aInA, b, bInB, rLessSum⟩138  . exact qLessR139140theorem realAddCut.proper (A B : Real)141  shows realAddCut(A, B) ≠ ℚ142proof143  have cutA := Real.characterization.forward at A with assumption144  have cutB := Real.characterization.forward at B with assumption145  have properA := DedekindCut.proper with cutA146  have properB := DedekindCut.proper with cutB147  obtain ⟨u, uInQ, uMissing⟩ := ProperSubset.missing with properA148  obtain ⟨v, vInQ, vMissing⟩ := ProperSubset.missing with properB149  have uRational : Rational(u) by exact uInQ150  have vRational : Rational(v) by exact vInQ151  have upperRational := rationalAddValue.rational_raw with uRational, vRational152  intro allRationals153  have upperInSum : rationalAddValue(u, v) ∈ realAddCut(A, B)154    rw allRationals155    exact upperRational156  obtain ⟨upperInQ, a, aInA, b, bInB, upperLessSum⟩ := realAddCut.membership.forward with upperInSum157  have subsetA := DedekindCut.subset_rationals with cutA158  have subsetB := DedekindCut.subset_rationals with cutB159  have aRational : Rational(a)160    unfold Rational161    exact subsetA with a, aInA162  have bRational : Rational(b)163    unfold Rational164    exact subsetB with b, bInB165  have aLessU := DedekindCut.lt_missing with cutA, aInA, uInQ, uMissing166  have bLessV := DedekindCut.lt_missing with cutB, bInB, vInQ, vMissing167  have first := rationalLess.add_right with aRational, uRational, bRational, aLessU168  have second := rationalLess.add_left with bRational, vRational, uRational, bLessV169  rw [rationalAddValue.notation, rationalAddValue.notation] at first170  rw [rationalAddValue.notation, rationalAddValue.notation] at second171  have sumRational := rationalAddValue.rational_raw with aRational, bRational172  have middleRational := rationalAddValue.rational_raw with uRational, bRational173  have sumInQ := sumRational174  have middleInQ := middleRational175  have transitive := rationalLess.transitive_on176  have sumLessUpper := transitive with177    rationalAddValue(a, b), sumInQ,178    rationalAddValue(u, b), middleInQ,179    rationalAddValue(u, v), upperInQ,180    first, second181  unfold rationalAddValue at upperLessSum182  unfold rationalAddValue at sumLessUpper183  unfold rationalAddValue at upperInQ184  unfold rationalAddValue at sumInQ185  have cycle := transitive with186    rationalAdd((u, v)), upperInQ,187    rationalAdd((a, b)), sumInQ,188    rationalAdd((u, v)), upperInQ,189    upperLessSum, sumLessUpper190  have irreflexive := rationalLess.irreflexive_on191  exact irreflexive with rationalAdd((u, v)), upperInQ, cycle192193theorem realAddCut.cut (A B : Real)194  shows DedekindCut(realAddCut(A, B))195proof196  have subset := realAddCut.subset_rationals at A, B197  have inhabited := realAddCut.nonempty at A, B with *198  have proper := realAddCut.proper at A, B with *199  unfold DedekindCut200  refine ⟨subset, inhabited, proper, _, _⟩201  . intros q qInSum p pInQ pLessQ202    exact realAddCut.downward with qInSum, pInQ, pLessQ203  . intros q qInSum204    exact realAddCut.no_greatest with qInSum205206theorem realAddCut.real (A B : Real)207  shows Real(realAddCut(A, B))208proof209  apply Real.characterization.backward210  exact realAddCut.cut with *211212-- Real addition as a set-valued function graph on pairs of cuts.213def realAdd : Set :=214  { p ∈ ((ℝ × ℝ) × ℝ) |215    ∃ A ∈ ℝ, ∃ B ∈ ℝ,216      p = ((A, B) ↦ realAddCut(A, B)) }217218def realAddValue (A B : Real) : Real := realAdd((A, B))219220theorem realAdd.relates (A B : Real)221  shows relates(realAdd, (A, B), realAddCut(A, B))222proof223  have realA : A ∈ ℝ by simp [Real]224  have realB : B ∈ ℝ by simp [Real]225  unfold relates226  apply realAdd.membership.backward227  constructor228  . apply product.pair at (A, B), realAddCut(A, B), ℝ × ℝ, ℝ229    . apply product.pair at A, B, ℝ, ℝ230      . exact realA231      . exact realB232    . exact realAddCut.real at A, B with *{2}233  . refine ⟨A, realA, B, realB, rfl⟩234235theorem realAdd.factors (input output : Set)236  requires mapped : relates(realAdd, input, output)237  shows ∃ A ∈ ℝ, ∃ B ∈ ℝ,238    input = (A, B) ∧ output = realAddCut(A, B)239proof240  unfold relates at mapped241  simp [realAdd.membership] at mapped242  rcases mapped with ⟨bounded, A, realA, B, realB, shape⟩243  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape244  refine ⟨A, realA, B, realB, inputShape, outputShape⟩245246theorem realAdd.total247  shows TotalBetween(realAdd, ℝ × ℝ, ℝ)248proof249  intros input inputInProduct250  obtain ⟨bounded, A, realA, B, realB, inputShape⟩ := product.membership.forward with inputInProduct251  have typedA : Real(A) by exact realA252  have typedB : Real(B) by exact realB253  witness realAddCut(A, B)254  constructor255  . exact realAddCut.real with typedA, typedB256  . rw inputShape257    exact realAdd.relates with typedA, typedB258259theorem realAdd.functional260  shows Functional(realAdd)261proof262  intros input y inputY z inputZ263  obtain ⟨A, realA, B, realB, inputFirst, outputFirst⟩ := realAdd.factors with inputY264  obtain ⟨C, realC, D, realD, inputSecond, outputSecond⟩ := realAdd.factors with inputZ265  rw inputFirst at inputSecond266  obtain ⟨sameLeft, sameRight⟩ := orderedPair.injective with inputSecond267  rw [outputFirst, outputSecond, sameLeft, sameRight]268  rfl269270theorem realAdd.function271  shows realAdd : ℝ × ℝ → ℝ272proof273  constructor274    intros p hp275    simp [realAdd.membership] at hp276    rcases hp with ⟨bounded, witnesses⟩277    exact bounded278  . constructor279    . exact realAdd.functional280    . exact realAdd.total281282instance realAdd.operation283  shows AddOperation(ℝ, realAdd)284proof285  exact realAdd.function286287notation infixl 60 "+" => call2 via AddOperation(ℝ, _) for Real288notation numeral "0" via OfNat(ℝ, 0, _) for Real289290theorem realAddValue.real (A B : Real)291  shows Real(A + B)292proof293  have realA : A ∈ ℝ by simp [Real]294  have realB : B ∈ ℝ by simp [Real]295  have input := product.pair with realA, realB296  obtain ⟨C, realC, mapped⟩ := FunctionBetween.exists_value with realAdd.function, input297  have applied := FunctionBetween.apply_value with realAdd.function, input, mapped298  unfold call2299  rw applied300  exact realC301302theorem realAddValue.cut (A B : Real)303  shows A + B = realAddCut(A, B)304proof305  have realA : A ∈ ℝ by simp [Real]306  have realB : B ∈ ℝ by simp [Real]307  have input := product.pair with realA, realB308  have mapped := realAdd.relates at A, B with *309  unfold call2310  exact FunctionBetween.apply_value with realAdd.function, input, mapped311312theorem realAddCut.commutative (A B : Real)313  shows realAddCut(A, B) = realAddCut(B, A)314proof315  ext q316  constructor317  . intro qInSum318    obtain ⟨qInQ, a, aInA, b, bInB, qLessSum⟩ := realAddCut.membership.forward with qInSum319    have cutA := Real.characterization.forward at A with assumption320    have cutB := Real.characterization.forward at B with assumption321    have subsetA := DedekindCut.subset_rationals with cutA322    have subsetB := DedekindCut.subset_rationals with cutB323    have aRational : Rational(a)324      unfold Rational325      exact subsetA with a, aInA326    have bRational : Rational(b)327      unfold Rational328      exact subsetB with b, bInB329    have sumComm := rationalAddValue.commutative with aRational, bRational330    unfold call2 at sumComm331    rw sumComm at qLessSum332    exact realAddCut.membership.backward with ⟨qInQ, b, bInB, a, aInA, qLessSum⟩333  . intro qInSum334    obtain ⟨qInQ2, b2, b2InB, a2, a2InA, qLessSum2⟩ := realAddCut.membership.forward with qInSum335    have cutA := Real.characterization.forward at A with assumption336    have cutB := Real.characterization.forward at B with assumption337    have subsetA := DedekindCut.subset_rationals with cutA338    have subsetB := DedekindCut.subset_rationals with cutB339    have a2Rational : Rational(a2)340      unfold Rational341      exact subsetA with a2, a2InA342    have b2Rational : Rational(b2)343      unfold Rational344      exact subsetB with b2, b2InB345    have sumComm2 := rationalAddValue.commutative with b2Rational, a2Rational346    unfold call2 at sumComm2347    rw sumComm2 at qLessSum2348    exact realAddCut.membership.backward with ⟨qInQ2, a2, a2InA, b2, b2InB, qLessSum2⟩349350theorem realAddCut.zero_right (A : Real)351  shows realAddCut(A, realZero) = A352proof353  ext q354  constructor355  . intro qInSum356    obtain ⟨qInQ, a, aInA, b, bInZero, qLessSum⟩ := realAddCut.membership.forward with qInSum357    unfold realZero at bInZero358    simp [rationalCut.membership] at bInZero359    rcases bInZero with ⟨bInQ, bLessZero⟩360    have cutA := Real.characterization.forward with assumption361    have subsetA := DedekindCut.subset_rationals with cutA362    have aInQ := subsetA with a, aInA363    have aRational : Rational(a) by exact aInQ364    have bRational : Rational(b) by exact bInQ365    have shifted := rationalLess.add_left with bRational, rationalZero.rational, aRational, bLessZero366    have identity := rationalAddValue.zero_right with aRational367    rw identity at shifted368    have sumRational := rationalAddValue.rational_raw with aRational, bRational369    have sumInQ := sumRational370    unfold rationalAddValue at sumInQ371    unfold call2 at shifted372    have transitive := rationalLess.transitive_on373    have qLessA := transitive with374      q, qInQ, rationalAdd((a, b)), sumInQ, a, aInQ,375      qLessSum, shifted376    exact DedekindCut.downward with cutA, aInA, qInQ, qLessA377  . intro qInA378    have cutA := Real.characterization.forward with assumption379    have subsetA := DedekindCut.subset_rationals with cutA380    have qInQ := subsetA with q, qInA381    obtain ⟨r, rInA, qLessR⟩ := DedekindCut.no_greatest with cutA, qInA382    have rInQ := subsetA with r, rInA383    have rRational : Rational(r) by exact rInQ384    obtain ⟨s, sInQ, qLessS, sLessR⟩ := rationalLess.dense with qLessR385    have sRational : Rational(s) by typecheck386    have differenceRational := rationalSubValue.rational with sRational, rRational387    have differenceNegative := rationalLess.sub_self_negative with sLessR388    have differenceInZero : s - r ∈ realZero389      unfold realZero390      simp [rationalCut.membership]391      constructor392        exact differenceRational393      . exact differenceNegative394    have sumShape := rationalAddValue.add_sub_cancel_left with rRational, sRational395    rw ← sumShape at qLessS396    unfold call2 at qLessS397    exact realAddCut.membership.backward with ⟨qInQ, r, rInA, s - r, differenceInZero, qLessS⟩398399theorem realAddCut.zero_left (A : Real)400  shows realAddCut(realZero, A) = A401proof402  calc403    realAddCut(realZero, A) = realAddCut(A, realZero) :=404      realAddCut.commutative with realZero.real405    _ = A := realAddCut.zero_right at A with assumption406407-- Associativity is proved at the level of cuts.  Density supplies an inner408-- witness close enough to the desired rational sum; no representative of a409-- real number or algebraic axiom is hidden in the argument.410theorem realAddCut.associative (A B C : Real)411  shows realAddCut(realAddCut(A, B), C) = realAddCut(A, realAddCut(B, C))412proof413  ext q414  constructor415  . intro qInLeft416    obtain ⟨qInQ, x, xInAB, c, cInC, qLessXC⟩ := realAddCut.membership_value.forward with qInLeft417    obtain ⟨xInQ, a, aInA, b, bInB, xLessAB⟩ := realAddCut.membership_value.forward with xInAB418    rw ← rationalAddValue.notation at qLessXC419    rw ← rationalAddValue.notation at xLessAB420    have cutA := Real.characterization.forward at A with assumption421    have cutB := Real.characterization.forward at B with assumption422    have cutC := Real.characterization.forward at C with assumption423    have subsetA := DedekindCut.subset_rationals with cutA424    have subsetB := DedekindCut.subset_rationals with cutB425    have subsetC := DedekindCut.subset_rationals with cutC426    have qRational : Rational(q) by exact qInQ427    have xRational : Rational(x) by exact xInQ428    have aRational : Rational(a)429      unfold Rational430      exact subsetA with a, aInA431    have bRational : Rational(b)432      unfold Rational433      exact subsetB with b, bInB434    have cRational : Rational(c)435      unfold Rational436      exact subsetC with c, cInC437    have abRational := rationalAddValue.rational with aRational, bRational438    have bcRational := rationalAddValue.rational with bRational, cRational439    have scaled := rationalLess.add_right with xRational, abRational, cRational, xLessAB440    have qLessABC := rationalLess.transitive with qLessXC, scaled441    rw rationalAddValue.associative at qLessABC442    have differenceLess := rationalLess.sub_left with qLessABC443    have differenceRational := rationalSubValue.rational with qRational, aRational444    obtain ⟨y, yInQ, differenceLessY, yLessBC⟩ := rationalLess.dense with445      differenceRational, bcRational, differenceLess446    have yInBC : y ∈ realAddCut(B, C)447      apply realAddCut.membership_value.backward448      rw rationalAddValue.notation at yLessBC449      refine ⟨yInQ, b, bInB, c, cInC, yLessBC⟩450    have qLessAY := rationalLess.add_left_of_sub_left with differenceLessY451    apply realAddCut.membership_value.backward452    rw rationalAddValue.notation at qLessAY453    refine ⟨qInQ, a, aInA, y, yInBC, qLessAY⟩454  . intro qInRight455    obtain ⟨qInQ2, a2, a2InA, y2, y2InBC, qLessAY2⟩ := realAddCut.membership_value.forward with qInRight456    obtain ⟨y2InQ, b2, b2InB, c2, c2InC, y2LessBC⟩ := realAddCut.membership_value.forward with y2InBC457    rw ← rationalAddValue.notation at qLessAY2458    rw ← rationalAddValue.notation at y2LessBC459    have cutA2 := Real.characterization.forward at A with assumption460    have cutB2 := Real.characterization.forward at B with assumption461    have cutC2 := Real.characterization.forward at C with assumption462    have subsetA2 := DedekindCut.subset_rationals with cutA2463    have subsetB2 := DedekindCut.subset_rationals with cutB2464    have subsetC2 := DedekindCut.subset_rationals with cutC2465    have qRational2 : Rational(q) by exact qInQ2466    have a2Rational : Rational(a2)467      unfold Rational468      exact subsetA2 with a2, a2InA469    have y2Rational : Rational(y2) by exact y2InQ470    have b2Rational : Rational(b2)471      unfold Rational472      exact subsetB2 with b2, b2InB473    have c2Rational : Rational(c2)474      unfold Rational475      exact subsetC2 with c2, c2InC476    have a2b2Rational := rationalAddValue.rational with a2Rational, b2Rational477    have b2c2Rational := rationalAddValue.rational with b2Rational, c2Rational478    have scaled2 := rationalLess.add_left with y2Rational, b2c2Rational, a2Rational, y2LessBC479    have qLessABC2 := rationalLess.transitive with qLessAY2, scaled2480    rw ← rationalAddValue.associative at qLessABC2481    have outerCommutative2 := rationalAddValue.commutative with a2b2Rational, c2Rational482    rw outerCommutative2 at qLessABC2483    have differenceLess2 := rationalLess.sub_left with qLessABC2484    have differenceRational2 := rationalSubValue.rational with qRational2, c2Rational485    obtain ⟨x2, x2InQ, differenceLessX2, x2LessAB⟩ := rationalLess.dense with486      differenceRational2, a2b2Rational, differenceLess2487    have x2Rational : Rational(x2) by typecheck488    have x2InAB : x2 ∈ realAddCut(A, B)489      apply realAddCut.membership_value.backward490      rw rationalAddValue.notation at x2LessAB491      refine ⟨x2InQ, a2, a2InA, b2, b2InB, x2LessAB⟩492    have qLessCX2 := rationalLess.add_left_of_sub_left with493      qRational2, c2Rational, x2Rational, differenceLessX2494    have innerCommutative2 := rationalAddValue.commutative with c2Rational, x2Rational495    rw innerCommutative2 at qLessCX2496    apply realAddCut.membership_value.backward497    rw rationalAddValue.notation at qLessCX2498    refine ⟨qInQ2, x2, x2InAB, c2, c2InC, qLessCX2⟩499500theorem realAddValue.commutative (A B : Real)501  shows A + B = B + A502proof503  calc504    A + B = realAddCut(A, B) :=505      realAddValue.cut with *{2}506    _ = realAddCut(B, A) :=507      realAddCut.commutative with *{2}508    _ = B + A := by simp [realAddValue.cut]509510theorem realAddValue.zero_right (A : Real)511  shows A + 0 = A512proof513  calc514    A + realZero = realAddCut(A, realZero) :=515      realAddValue.cut with realZero.real516    _ = A := realAddCut.zero_right at A with assumption517518theorem realAddValue.zero_left (A : Real)519  shows 0 + A = A520proof521  calc522    realZero + A = A + realZero :=523      realAddValue.commutative with realZero.real524    _ = A := realAddValue.zero_right at A with assumption525526theorem realAddValue.associative (A B C : Real)527  shows (A + B) + C = A + (B + C)528proof529  calc530    (A + B) + C = realAddCut(realAddCut(A, B), C) := by simp [realAddValue.cut]531    _ = realAddCut(A, realAddCut(B, C)) :=532      realAddCut.associative with *{3}533    _ = A + (B + C) := by simp [realAddValue.cut]534535-- The first bundled algebraic structure on the Dedekind reals.  It is a536-- checked theorem that elaboration registers as an instance.537instance realAdd.comm_monoid538  shows IsCommMonoid(ℝ, realAdd, realZero)539proof540  constructor541    constructor542      constructor543        exact realAdd.function544        intros A realA B realB C realC545        have typedA : Real(A) by exact realA546        have typedB : Real(B) by exact realB547        have typedC : Real(C) by exact realC548        exact realAddValue.associative with typedA, typedB, typedC549      constructor550      . exact realZero.real551      . intros A realA552        have typedA : Real(A) by exact realA553        constructor554        . exact realAddValue.zero_left with typedA555        . exact realAddValue.zero_right with typedA556    intros A realA B realB557    have typedA : Real(A) by exact realA558    have typedB : Real(B) by exact realB559    exact realAddValue.commutative with typedA, typedB560561theorem realAddValue.type (A B : Real)562  shows Real(realAddValue(A, B))563proof564  have closed := realAddValue.real at A, B with *565  unfold realAddValue566  unfold call2 at closed567  exact closed568