Grace/Cumulus/Int/Order.g17

Open in Workbench Download source

Imports

Ring · AbsoluteValue

Declarations

• IntegerNonnegative predicate
• IntegerPositive predicate
• integerLe predicate
• integerLess predicate
• IntegerNonnegative.ofNat theorem derivation
• IntegerNonnegative.integer theorem derivation
• IntegerNonnegative.zero theorem derivation
• IntegerNonnegative.one theorem derivation
• IntegerNonnegative.add theorem derivation
• IntegerNonnegative.mul theorem derivation
• IntegerNonnegative.negative_iff theorem derivation
• IntegerNonnegative.cases theorem derivation
• IntegerNonnegative.exists_natural theorem derivation
• IntegerNonnegative.eq_zero theorem derivation
• IntegerNonnegative.of_positive theorem derivation
• IntegerPositive.ofNat_add_one theorem derivation
• IntegerPositive.iff_sub_one theorem derivation
• IntegerPositive.mul theorem derivation
• IntegerPositive.add theorem derivation
• IntegerPositive.not_zero theorem derivation
• integerLe.reflexive theorem derivation
• integerLe.of_eq theorem derivation
• integerLe.transitive theorem derivation
• integerLe.antisymmetric theorem derivation
• integerLe.total theorem derivation
• integerLe.zero_iff theorem derivation
• integerLe.sub_nonneg_iff theorem derivation
• integerLe.ofNat_nonneg theorem derivation
• integerLe.negative_nonpos theorem derivation
• integerLe.zero_one theorem derivation
• integerLe.add_right theorem derivation
• integerLe.add_left theorem derivation
• integerLe.add theorem derivation
• integerLe.add_right_cancel theorem derivation
• integerLe.add_left_cancel theorem derivation
• integerLe.neg theorem derivation
• integerLe.neg_nonneg_iff theorem derivation
• integerLe.sub_right theorem derivation
• integerLe.sub_left theorem derivation
• integerLe.exists_natural theorem derivation
• integerLe.of_natural theorem derivation
• integerLe.ofNat_iff theorem derivation
• integerLe.cases_sign theorem derivation
• integerLe.exists_negative theorem derivation
• integerLess.iff_add_one_le theorem derivation
• integerLess.zero_iff_positive theorem derivation
• integerLess.sub_positive_iff theorem derivation
• integerLess.add_one theorem derivation
• integerLe.add_one theorem derivation
• integerLess.implies_le theorem derivation
• integerLess.irreflexive theorem derivation
• integerLess.ne theorem derivation
• integerLess.transitive_le theorem derivation
• integerLe.transitive_less theorem derivation
• integerLess.transitive theorem derivation
• integerLess.of_le_ne theorem derivation
• integerLess.iff_le_ne theorem derivation
• integerLe.cases theorem derivation
• integerLe.not_less theorem derivation
• integerLess.not_le theorem derivation
• integerLess.asymmetric theorem derivation
• integerLe.of_not_less theorem derivation
• integerLess.of_not_le theorem derivation
• integerLess.trichotomy theorem derivation
• integerLess.add_right theorem derivation
• integerLess.add_left theorem derivation
• integerLess.add_le theorem derivation
• integerLe.add_less theorem derivation
• integerLess.add theorem derivation
• integerLess.add_right_cancel theorem derivation
• integerLess.neg theorem derivation
• integerLess.zero_one theorem derivation
• integerLess.ofNat_iff theorem derivation
• integerLess.one_le_of_positive theorem derivation
• integerLess.not_between theorem derivation

Source

1-- The order of the integers: nonnegative integers, ≤, and <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 Grace.Cumulus.Int.Order8import Ring9import AbsoluteValue1011predicate IntegerNonnegative (z : Set) := ∃ n ∈ ℕ, z = integerOfNat(n)12predicate IntegerPositive (z : Set) := ∃ n ∈ ℕ, z = integerOfNat(n + 1)1314predicate integerLe (x y : Integer) := IntegerNonnegative(y - x)15notation infix 50 "≤" => integerLe for Integer16notation infix 50 "≥" => reverse integerLe for Integer1718predicate integerLess (x y : Integer) := integerLe(x + 1, y)19notation infix 50 "<" => integerLess for Integer2021theorem IntegerNonnegative.ofNat (n : Nat)22  shows IntegerNonnegative(integerOfNat(n))23proof24  witness n25  constructor26  . typecheck27  . rfl2829theorem IntegerNonnegative.integer (z : Set)30  requires nonnegative : IntegerNonnegative(z)31  shows Integer(z)32proof33  obtain ⟨n, nMember, shape⟩ := nonnegative34  have nNat := nat.omega.backward with nMember35  rw shape36  exact integerOfNat.integer with *3738theorem IntegerNonnegative.zero39  shows IntegerNonnegative(integerZero)40proof41  have value := IntegerNonnegative.ofNat at 042  rw integerOfNat.zero at value43  exact value4445theorem IntegerNonnegative.one46  shows IntegerNonnegative(integerOne)47proof48  have value := IntegerNonnegative.ofNat at 149  unfold integerOne50  exact value5152theorem IntegerNonnegative.add (x y : Integer)53  requires first : IntegerNonnegative(x)54  requires second : IntegerNonnegative(y)55  shows IntegerNonnegative(x + y)56proof57  obtain ⟨n, nMember, xShape⟩ := first58  obtain ⟨m, mMember, yShape⟩ := second59  have nNat := nat.omega.backward with nMember60  have mNat := nat.omega.backward with mMember61  have sum := integerOfNat.add at n, m62  rw [xShape, yShape, ← sum]63  exact IntegerNonnegative.ofNat with *6465theorem IntegerNonnegative.mul (x y : Integer)66  requires first : IntegerNonnegative(x)67  requires second : IntegerNonnegative(y)68  shows IntegerNonnegative(x * y)69proof70  obtain ⟨n, nMember, xShape⟩ := first71  obtain ⟨m, mMember, yShape⟩ := second72  have nNat := nat.omega.backward with nMember73  have mNat := nat.omega.backward with mMember74  have product := integerMulValue.ofNat at n, m75  rw [xShape, yShape, product]76  exact IntegerNonnegative.ofNat with *7778theorem IntegerNonnegative.negative_iff (n : Nat)79  shows IntegerNonnegative(integerNegativeOfNat(n)) ↔ n = 080proof81  constructor82  . intro nonnegative83    obtain ⟨m, mMember, shape⟩ := nonnegative84    have mNat := nat.omega.backward with mMember85    symm at shape86    have both := integerOfNat.eq_negative with shape87    exact both.right88  . intro zero89    rw zero90    have same : integerNegativeOfNat(0) = integerOfNat(0)91      simp [integerNegativeOfNat, integerOfNat]92    rw same93    exact IntegerNonnegative.ofNat with *9495theorem IntegerNonnegative.cases (z : Integer)96  shows IntegerNonnegative(z) ∨ IntegerNonnegative(-z)97proof98  obtain ⟨n, nNat, sign⟩ := Integer.signed_natural at z with *99  cases sign with positive | negative100  . left101    rw positive102    exact IntegerNonnegative.ofNat with *103  . right104    rw negative105    have flipped := integerNegativeOfNat.neg at n106    rw flipped107    exact IntegerNonnegative.ofNat with *108109theorem IntegerNonnegative.exists_natural (z : Integer)110  requires nonnegative : IntegerNonnegative(z)111  shows ∃ n, Nat(n) ∧ z = integerOfNat(n)112proof113  obtain ⟨n, nMember, shape⟩ := nonnegative114  have nNat := nat.omega.backward with nMember115  exact ⟨n, nNat, shape⟩116117theorem IntegerNonnegative.eq_zero (z : Integer)118  requires first : IntegerNonnegative(z)119  requires second : IntegerNonnegative(-z)120  shows z = 0121proof122  obtain ⟨n, nMember, zShape⟩ := first123  obtain ⟨m, mMember, negShape⟩ := second124  have nNat := nat.omega.backward with nMember125  have mNat := nat.omega.backward with mMember126  have cancel : z + (-z) = 0 by ring127  rw [negShape, zShape] at cancel128  have sum := integerOfNat.add at n, m129  rw [← sum, ← integerOfNat.zero] at cancel130  have sumZero := integerOfNat.injective with cancel131  have both := add.eq_zero with sumZero132  rw [zShape, both.left]133  exact integerOfNat.zero134135theorem IntegerNonnegative.of_positive (z : Integer)136  requires positive : IntegerPositive(z)137  shows IntegerNonnegative(z)138proof139  obtain ⟨n, nMember, shape⟩ := positive140  have nNat := nat.omega.backward with nMember141  rw shape142  exact IntegerNonnegative.ofNat with *143144theorem IntegerPositive.ofNat_add_one (n : Nat)145  shows IntegerPositive(integerOfNat(n + 1))146proof147  witness n148  constructor149  . typecheck150  . rfl151152theorem IntegerPositive.iff_sub_one (z : Integer)153  shows IntegerPositive(z) ↔ IntegerNonnegative(z - 1)154proof155  constructor156  . intro positive157    obtain ⟨n, nMember, shape⟩ := positive158    have nNat := nat.omega.backward with nMember159    have split := integerOfNat.add at n, 1160    have one : integerOfNat(1) = 1161      unfold integerOne162      rfl163    rw [shape, split, one]164    have cancel : integerOfNat(n) + 1 - 1 = integerOfNat(n) by ring165    rw cancel166    exact IntegerNonnegative.ofNat with *167  . intro nonnegative168    obtain ⟨n, nMember, shape⟩ := nonnegative169    have nNat := nat.omega.backward with nMember170    have split := integerOfNat.add at n, 1171    have one : integerOfNat(1) = 1172      unfold integerOne173      rfl174    have restore : z = (z - 1) + 1 by ring175    rw [restore, shape, ← one, ← split]176    exact IntegerPositive.ofNat_add_one with *177178theorem IntegerPositive.mul (x y : Integer)179  requires first : IntegerPositive(x)180  requires second : IntegerPositive(y)181  shows IntegerPositive(x * y)182proof183  obtain ⟨n, nMember, xShape⟩ := first184  obtain ⟨m, mMember, yShape⟩ := second185  have nNat := nat.omega.backward with nMember186  have mNat := nat.omega.backward with mMember187  have product := integerMulValue.ofNat at n + 1, m + 1188  have expand : (n + 1) * (m + 1) = (n * m + n + m) + 1 by ring189  rw [xShape, yShape, product, expand]190  exact IntegerPositive.ofNat_add_one with *191192theorem IntegerPositive.add (x y : Integer)193  requires first : IntegerPositive(x)194  requires second : IntegerPositive(y)195  shows IntegerPositive(x + y)196proof197  obtain ⟨n, nMember, xShape⟩ := first198  obtain ⟨m, mMember, yShape⟩ := second199  have nNat := nat.omega.backward with nMember200  have mNat := nat.omega.backward with mMember201  have sum := integerOfNat.add at n + 1, m + 1202  have expand : (n + 1) + (m + 1) = (n + m + 1) + 1 by ring203  rw [xShape, yShape, ← sum, expand]204  exact IntegerPositive.ofNat_add_one with *205206theorem IntegerPositive.not_zero207  shows ¬IntegerPositive(integerZero)208proof209  intro positive210  obtain ⟨n, nMember, shape⟩ := positive211  have nNat := nat.omega.backward with nMember212  rw ← integerOfNat.zero at shape213  have same := integerOfNat.injective with shape214  have impossible : 0 < 0 by linarith215  exact Less.irreflexive with impossible216217theorem integerLe.reflexive (x : Integer)218  shows x ≤ x219proof220  unfold integerLe221  have zero : x - x = 0 by ring222  rw zero223  exact IntegerNonnegative.zero224225theorem integerLe.of_eq (x y : Integer)226  requires same : x = y227  shows x ≤ y228proof229  rw same230  exact integerLe.reflexive with *231232theorem integerLe.transitive (x y z : Integer)233  requires first : x ≤ y234  requires second : y ≤ z235  shows x ≤ z236proof237  unfold integerLe at first238  unfold integerLe at second239  have sum : z - x = (z - y) + (y - x) by ring240  unfold integerLe241  rw sum242  exact IntegerNonnegative.add with second, first243244theorem integerLe.antisymmetric (x y : Integer)245  requires first : x ≤ y246  requires second : y ≤ x247  shows x = y248proof249  unfold integerLe at first250  unfold integerLe at second251  have flip : x - y = -(y - x) by ring252  rw flip at second253  have zero := IntegerNonnegative.eq_zero with first, second254  have restore : x = y - (y - x) by ring255  rw [restore, zero]256  ring257258theorem integerLe.total (x y : Integer)259  shows x ≤ y ∨ y ≤ x260proof261  have split := IntegerNonnegative.cases at y - x with *262  cases split with forward | backward263  . left264    exact forward265  . right266    have flip : x - y = -(y - x) by ring267    unfold integerLe268    rw flip269    exact backward270271theorem integerLe.zero_iff (x : Integer)272  shows 0 ≤ x ↔ IntegerNonnegative(x)273proof274  have shape : x - 0 = x by ring275  constructor276  . intro below277    unfold integerLe at below278    rw shape at below279    exact below280  . intro nonnegative281    unfold integerLe282    rw shape283    exact nonnegative284285theorem integerLe.sub_nonneg_iff (x y : Integer)286  shows x ≤ y ↔ 0 ≤ y - x287proof288  have difference := integerLe.zero_iff at y - x with *289  constructor290  . intro below291    unfold integerLe at below292    exact difference.backward with below293  . intro below294    have nonnegative := difference.forward with below295    unfold integerLe296    exact nonnegative297298theorem integerLe.ofNat_nonneg (n : Nat)299  shows 0 ≤ integerOfNat(n)300proof301  apply integerLe.zero_iff.backward302  exact IntegerNonnegative.ofNat with *303304theorem integerLe.negative_nonpos (n : Nat)305  shows integerNegativeOfNat(n) ≤ 0306proof307  unfold integerLe308  have flip : 0 - integerNegativeOfNat(n) = -(integerNegativeOfNat(n)) by ring309  rw [flip, integerNegativeOfNat.neg]310  exact IntegerNonnegative.ofNat with *311312theorem integerLe.zero_one313  shows integerZero ≤ integerOne314proof315  unfold integerLe316  have shape : integerOne - integerZero = integerOne by ring317  rw shape318  exact IntegerNonnegative.one319320theorem integerLe.add_right (x y z : Integer)321  requires below : x ≤ y322  shows x + z ≤ y + z323proof324  have shape : (y + z) - (x + z) = y - x by ring325  unfold integerLe326  rw shape327  exact below328329theorem integerLe.add_left (x y z : Integer)330  requires below : x ≤ y331  shows z + x ≤ z + y332proof333  have shape : (z + y) - (z + x) = y - x by ring334  unfold integerLe335  rw shape336  exact below337338theorem integerLe.add (a b c d : Integer)339  requires first : a ≤ b340  requires second : c ≤ d341  shows a + c ≤ b + d342proof343  have left := integerLe.add_right at a, b, c with first344  have right := integerLe.add_left at c, d, b with second345  exact integerLe.transitive with left, right346347theorem integerLe.add_right_cancel (x y z : Integer)348  requires below : x + z ≤ y + z349  shows x ≤ y350proof351  have shape : (y + z) - (x + z) = y - x by ring352  unfold integerLe at below353  rw shape at below354  exact below355356theorem integerLe.add_left_cancel (x y z : Integer)357  requires below : z + x ≤ z + y358  shows x ≤ y359proof360  have shape : (z + y) - (z + x) = y - x by ring361  unfold integerLe at below362  rw shape at below363  exact below364365theorem integerLe.neg (x y : Integer)366  shows x ≤ y ↔ -y ≤ -x367proof368  have shape : (-x) - (-y) = y - x by ring369  constructor370  . intro below371    unfold integerLe372    rw shape373    exact below374  . intro below375    unfold integerLe at below376    rw shape at below377    exact below378379theorem integerLe.neg_nonneg_iff (x : Integer)380  shows 0 ≤ -x ↔ x ≤ 0381proof382  have shape : (-x) - 0 = 0 - x by ring383  constructor384  . intro below385    unfold integerLe at below386    rw shape at below387    exact below388  . intro below389    unfold integerLe390    rw shape391    exact below392393theorem integerLe.sub_right (x y z : Integer)394  requires below : x ≤ y395  shows x - z ≤ y - z396proof397  have shape : (y - z) - (x - z) = y - x by ring398  unfold integerLe399  rw shape400  exact below401402theorem integerLe.sub_left (x y z : Integer)403  requires below : x ≤ y404  shows z - y ≤ z - x405proof406  have shape : (z - x) - (z - y) = y - x by ring407  unfold integerLe408  rw shape409  exact below410411theorem integerLe.exists_natural (x y : Integer)412  requires below : x ≤ y413  shows ∃ n, Nat(n) ∧ y = x + integerOfNat(n)414proof415  unfold integerLe at below416  obtain ⟨n, nNat, shape⟩ := IntegerNonnegative.exists_natural with below417  witness n418  have restore : y = x + (y - x) by ring419  rw [restore, shape]420  rfl421422theorem integerLe.of_natural (x y : Integer, n : Nat)423  requires shape : y = x + integerOfNat(n)424  shows x ≤ y425proof426  unfold integerLe427  rw shape428  have cancel : x + integerOfNat(n) - x = integerOfNat(n) by ring429  rw cancel430  exact IntegerNonnegative.ofNat with *431432theorem integerLe.ofNat_iff (a b : Nat)433  shows integerOfNat(a) ≤ integerOfNat(b) ↔ a ≤ b434proof435  constructor436  . intro below437    obtain ⟨n, nNat, shape⟩ := integerLe.exists_natural with below438    have sum := integerOfNat.add at a, n439    rw ← sum at shape440    have same := integerOfNat.injective with shape441    witness n442    symm443    exact same444  . intro below445    obtain ⟨n, nNat, equation⟩ := below446    have sum := integerOfNat.add at a, n447    apply integerLe.of_natural at integerOfNat(a), integerOfNat(b), n448    rw [← sum, equation]449    rfl450451theorem integerLe.cases_sign (x : Integer)452  shows 0 ≤ x ∨ x ≤ 0453proof454  have split := IntegerNonnegative.cases at x with *455  cases split with nonnegative | negative456  . left457    exact integerLe.zero_iff.backward with nonnegative458  . right459    have lifted := integerLe.zero_iff.backward with negative460    exact integerLe.neg_nonneg_iff.forward with lifted461462theorem integerLe.exists_negative (x : Integer)463  requires nonpositive : x ≤ 0464  shows ∃ n, Nat(n) ∧ x = integerNegativeOfNat(n)465proof466  have negated := integerLe.neg_nonneg_iff.backward with nonpositive467  have nonnegative := integerLe.zero_iff.forward with negated468  obtain ⟨n, nNat, shape⟩ :=469    IntegerNonnegative.exists_natural with nonnegative470  witness n471  have restore : x = -(-x) by ring472  rw [restore, shape]473  exact integerOfNat.neg with *474475theorem integerLess.iff_add_one_le (x y : Integer)476  shows x < y ↔ x + 1 ≤ y477proof478  constructor479  . intro below480    unfold integerLess at below481    exact below482  . intro below483    unfold integerLess484    exact below485486theorem integerLess.zero_iff_positive (x : Integer)487  shows 0 < x ↔ IntegerPositive(x)488proof489  have shape : x - (integerZero + 1) = x - 1 by ring490  have positive := IntegerPositive.iff_sub_one at x with *491  constructor492  . intro below493    unfold integerLess at below494    unfold integerLe at below495    rw shape at below496    exact positive.backward with below497  . intro isPositive498    have nonnegative := positive.forward with isPositive499    unfold integerLess500    unfold integerLe501    rw shape502    exact nonnegative503504theorem integerLess.sub_positive_iff (x y : Integer)505  shows x < y ↔ 0 < y - x506proof507  have shape : y - (x + 1) = (y - x) - (integerZero + 1) by ring508  constructor509  . intro below510    unfold integerLess at below511    unfold integerLe at below512    rw shape at below513    unfold integerLess514    unfold integerLe515    exact below516  . intro below517    unfold integerLess at below518    unfold integerLe at below519    unfold integerLess520    unfold integerLe521    rw shape522    exact below523524theorem integerLess.add_one (x : Integer)525  shows x < x + 1526proof527  unfold integerLess528  exact integerLe.reflexive with *529530theorem integerLe.add_one (x : Integer)531  shows x ≤ x + 1532proof533  apply integerLe.of_natural at x, x + 1, 1534  unfold integerOne535  rfl536537theorem integerLess.implies_le (x y : Integer)538  requires below : x < y539  shows x ≤ y540proof541  unfold integerLess at below542  have step := integerLe.add_one at x543  exact integerLe.transitive with step, below544545theorem integerLess.irreflexive (x : Integer)546  shows ¬x < x547proof548  intro below549  unfold integerLess at below550  unfold integerLe at below551  have shape : x - (x + 1) = integerNegativeOfNat(1)552    have flipped := integerOfNat.neg at 1553    unfold integerOne554    rw ← flipped555    ring556  rw shape at below557  have zero := IntegerNonnegative.negative_iff.forward with below558  have impossible : 0 < 1 by linarith559  rw zero at impossible560  exact Less.irreflexive with impossible561562theorem integerLess.ne (x y : Integer)563  requires below : x < y564  shows x ≠ y565proof566  intro same567  rw same at below568  exact integerLess.irreflexive with below569570theorem integerLess.transitive_le (x y z : Integer)571  requires first : x < y572  requires second : y ≤ z573  shows x < z574proof575  unfold integerLess at first576  unfold integerLess577  exact integerLe.transitive with first, second578579theorem integerLe.transitive_less (x y z : Integer)580  requires first : x ≤ y581  requires second : y < z582  shows x < z583proof584  unfold integerLess at second585  unfold integerLess586  have step := integerLe.add_right at x, y, integerOne with first587  exact integerLe.transitive with step, second588589theorem integerLess.transitive (x y z : Integer)590  requires first : x < y591  requires second : y < z592  shows x < z593proof594  have weak := integerLess.implies_le with second595  exact integerLess.transitive_le with first, weak596597theorem integerLess.of_le_ne (x y : Integer)598  requires below : x ≤ y599  requires distinct : x ≠ y600  shows x < y601proof602  obtain ⟨n, nNat, shape⟩ := integerLe.exists_natural with below603  have split := natural.zero_or_successor at n604  cases split with zero | successor605  . rw [zero, integerOfNat.zero] at shape606    have same : x = y607      rw shape608      ring609    exfalso610    exact distinct with same611  . obtain ⟨k, kNat, equation⟩ := successor612    have step : succ(k) = k + 1 by ring613    rw [equation, step] at shape614    have sum := integerOfNat.add at k, 1615    have one : integerOfNat(1) = 1616      unfold integerOne617      rfl618    rw [sum, one] at shape619    unfold integerLess620    apply integerLe.of_natural at x + 1, y, k621    rw shape622    ring623624theorem integerLess.iff_le_ne (x y : Integer)625  shows x < y ↔ x ≤ y ∧ x ≠ y626proof627  constructor628  . intro below629    exact ⟨integerLess.implies_le with below, integerLess.ne with below⟩630  . intro both631    exact integerLess.of_le_ne with both.left, both.right632633theorem integerLe.cases (x y : Integer)634  requires below : x ≤ y635  shows x < y ∨ x = y636proof637  have split : x = y ∨ x ≠ y by tauto638  cases split with same | distinct639  . right640    exact same641  . left642    exact integerLess.of_le_ne with below, distinct643644theorem integerLe.not_less (x y : Integer)645  requires below : x ≤ y646  shows ¬y < x647proof648  intro above649  have cycle := integerLess.transitive_le with above, below650  exact integerLess.irreflexive with cycle651652theorem integerLess.not_le (x y : Integer)653  requires below : x < y654  shows ¬y ≤ x655proof656  intro above657  have cycle := integerLess.transitive_le with below, above658  exact integerLess.irreflexive with cycle659660theorem integerLess.asymmetric (x y : Integer)661  requires below : x < y662  shows ¬y < x663proof664  have weak := integerLess.implies_le with below665  exact integerLe.not_less with weak666667theorem integerLe.of_not_less (x y : Integer)668  requires notBelow : ¬x < y669  shows y ≤ x670proof671  have total := integerLe.total at x, y672  cases total with below | above673  . have split := integerLe.cases with below674    cases split with strict | same675    . exfalso676      exact notBelow with strict677    . rw same678      exact integerLe.reflexive with *679  . exact above680681theorem integerLess.of_not_le (x y : Integer)682  requires notBelow : ¬x ≤ y683  shows y < x684proof685  have total := integerLe.total at x, y686  cases total with below | above687  . exfalso688    exact notBelow with below689  . have distinct : y ≠ x690      intro same691      rw same at notBelow692      exact notBelow with (integerLe.reflexive at x)693    exact integerLess.of_le_ne with above, distinct694695theorem integerLess.trichotomy (x y : Integer)696  shows x < y ∨ x = y ∨ y < x697proof698  have total := integerLe.total at x, y699  cases total with below | above700  . have split := integerLe.cases with below701    cases split with strict | same702    . left703      exact strict704    . right705      left706      exact same707  . have split := integerLe.cases with above708    cases split with strict | same709    . right710      right711      exact strict712    . right713      left714      symm715      exact same716717theorem integerLess.add_right (x y z : Integer)718  requires below : x < y719  shows x + z < y + z720proof721  unfold integerLess at below722  unfold integerLess723  have shape : x + z + 1 = (x + 1) + z by ring724  rw shape725  exact integerLe.add_right with below726727theorem integerLess.add_left (x y z : Integer)728  requires below : x < y729  shows z + x < z + y730proof731  have shifted := integerLess.add_right at x, y, z with below732  have left : x + z = z + x by ring733  have right : y + z = z + y by ring734  rw [left, right] at shifted735  exact shifted736737theorem integerLess.add_le (a b c d : Integer)738  requires first : a < b739  requires second : c ≤ d740  shows a + c < b + d741proof742  have left := integerLess.add_right at a, b, c with first743  have right := integerLe.add_left at c, d, b with second744  exact integerLess.transitive_le with left, right745746theorem integerLe.add_less (a b c d : Integer)747  requires first : a ≤ b748  requires second : c < d749  shows a + c < b + d750proof751  have left := integerLe.add_right at a, b, c with first752  have right := integerLess.add_left at c, d, b with second753  exact integerLe.transitive_less with left, right754755theorem integerLess.add (a b c d : Integer)756  requires first : a < b757  requires second : c < d758  shows a + c < b + d759proof760  have weak := integerLess.implies_le with second761  exact integerLess.add_le with first, weak762763theorem integerLess.add_right_cancel (x y z : Integer)764  requires below : x + z < y + z765  shows x < y766proof767  have shifted := integerLess.add_right at x + z, y + z, -z with below768  have left : x + z + (-z) = x by ring769  have right : y + z + (-z) = y by ring770  rw [left, right] at shifted771  exact shifted772773theorem integerLess.neg (x y : Integer)774  shows x < y ↔ -y < -x775proof776  have shape : (-x) - (-y + 1) = y - (x + 1) by ring777  constructor778  . intro below779    unfold integerLess at below780    unfold integerLe at below781    unfold integerLess782    unfold integerLe783    rw shape784    exact below785  . intro below786    unfold integerLess at below787    unfold integerLe at below788    rw shape at below789    unfold integerLess790    unfold integerLe791    exact below792793theorem integerLess.zero_one794  shows integerZero < integerOne795proof796  unfold integerLess797  have shape : integerZero + 1 = integerOne by ring798  rw shape799  exact integerLe.reflexive with *800801theorem integerLess.ofNat_iff (a b : Nat)802  shows integerOfNat(a) < integerOfNat(b) ↔ a < b803proof804  have sum := integerOfNat.add at a, 1805  have one : integerOfNat(1) = 1806    unfold integerOne807    rfl808  have gap := Less.gap at a, b809  have bridge := integerLe.ofNat_iff at a + 1, b810  constructor811  . intro below812    unfold integerLess at below813    rw [← one, ← sum] at below814    have weak := bridge.forward with below815    exact gap.backward with weak816  . intro below817    have weak := gap.forward with below818    have lifted := bridge.backward with weak819    unfold integerLess820    rw [← one, ← sum]821    exact lifted822823theorem integerLess.one_le_of_positive (x : Integer)824  requires positive : 0 < x825  shows 1 ≤ x826proof827  unfold integerLess at positive828  have shape : integerZero + 1 = integerOne by ring829  rw shape at positive830  exact positive831832theorem integerLess.not_between (x y : Integer)833  requires first : x < y834  requires second : y < x + 1835  shows ⊥836proof837  unfold integerLess at first838  unfold integerLess at second839  have cancelled := integerLe.add_right_cancel at y, x, integerOne with second840  have cycle := integerLe.transitive with first, cancelled841  exact integerLess.irreflexive at x with cycle842