Grace/Cumulus/Nat/OrderLemmas.g17

Open in Workbench Download source

Imports

Order

Declarations

• LessEqual.of_eq theorem derivation
• LessEqual.exists_add theorem derivation
• Less.ne theorem derivation
• Less.ne_reverse theorem derivation
• Less.of_LessEqual_ne theorem derivation
• Less.iff_LessEqual_ne theorem derivation
• LessEqual.cases theorem derivation
• LessEqual.iff_Less_or_eq theorem derivation
• LessEqual.not_Less theorem derivation
• Less.not_LessEqual theorem derivation
• Less.asymmetric theorem derivation
• LessEqual.iff_not_Less theorem derivation
• Less.iff_not_LessEqual theorem derivation
• LessEqual.antisymmetric_iff theorem derivation
• Less.or_LessEqual theorem derivation
• Less.not_below_zero theorem derivation
• LessEqual.eq_zero theorem derivation
• LessEqual.zero_iff theorem derivation
• Less.positive_of_ne_zero theorem derivation
• Less.ne_zero_of_positive theorem derivation
• Less.positive_iff theorem derivation
• LessEqual.one_of_positive theorem derivation
• LessEqual.one_iff_positive theorem derivation
• LessEqual.one_iff_ne_zero theorem derivation
• Less.zero_one theorem derivation
• Less.add_one theorem derivation
• LessEqual.add_one theorem derivation
• Less.add_one_iff theorem derivation
• LessEqual.add_one_iff theorem derivation
• Less.add_one_both_iff theorem derivation
• LessEqual.add_left_self theorem derivation
• LessEqual.add_monotone_left theorem derivation
• LessEqual.add_right_iff theorem derivation
• LessEqual.add_left_iff theorem derivation
• Less.add_monotone_right theorem derivation
• Less.add_monotone_left theorem derivation
• Less.add_left_cancel theorem derivation
• Less.add_right_iff theorem derivation
• Less.add_left_iff theorem derivation
• LessEqual.of_add_left theorem derivation
• LessEqual.of_add_right theorem derivation
• Less.of_add_left theorem derivation
• Less.of_add_right theorem derivation
• Less.add_positive_left theorem derivation
• Less.add_positive_right theorem derivation
• LessEqual.double theorem derivation
• Less.double_of_positive theorem derivation
• LessEqual.mul_right theorem derivation
• LessEqual.mul theorem derivation
• Less.mul_right theorem derivation
• Less.mul theorem derivation
• Less.mul_positive theorem derivation
• mul.positive_iff theorem derivation
• mul.eq_zero_iff theorem derivation
• LessEqual.mul_left_cancel_positive theorem derivation
• LessEqual.mul_right_cancel_positive theorem derivation
• Less.mul_right_cancel_positive theorem derivation
• LessEqual.le_mul_left theorem derivation
• LessEqual.le_mul_right theorem derivation
• LessEqual.one_le_mul theorem derivation
• LessEqual.mul_self theorem derivation
• mul.eq_one theorem derivation
• Less.one_lt_iff theorem derivation
• Less.exists_add_one theorem derivation
• Less.add_one_le_of_lt theorem derivation
• Less.of_add_one_le theorem derivation
• Less.lt_of_lt_of_eq theorem derivation
• LessEqual.le_of_le_of_eq theorem derivation

Source

1-- Everyday order lemmas on the natural 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.Nat.OrderLemmas8import Order910theorem LessEqual.of_eq (a b : Nat)11  requires same : a = b12  shows a ≤ b13proof14  rw same15  exact LessEqual.reflexive with *1617theorem LessEqual.exists_add (a b : Nat)18  requires below : a ≤ b19  shows ∃ k, Nat(k) ∧ b = a + k20proof21  obtain ⟨k, kNat, equation⟩ := below22  witness k23  symm24  exact equation2526theorem Less.ne (a b : Nat)27  requires below : a < b28  shows a ≠ b29proof30  intro same31  rw same at below32  have excluded := Less.irreflexive at b33  exact excluded with below3435theorem Less.ne_reverse (a b : Nat)36  requires below : a < b37  shows b ≠ a38proof39  intro same40  rw same at below41  have excluded := Less.irreflexive at a42  exact excluded with below4344theorem Less.of_LessEqual_ne (a b : Nat)45  requires below : a ≤ b46  requires distinct : a ≠ b47  shows a < b48proof49  have comparison := Less.trichotomy at a, b with *50  rcases comparison with less | equal | greater51  . exact less52  . exfalso53    exact distinct with equal54  . have weak := Less.implies_LessEqual with greater55    have same := LessEqual.antisymmetric with below, weak56    exfalso57    exact distinct with same5859theorem Less.iff_LessEqual_ne (a b : Nat)60  shows a < b ↔ a ≤ b ∧ a ≠ b61proof62  constructor63  . intro below64    exact ⟨Less.implies_LessEqual with below, Less.ne with below⟩65  . intro both66    exact Less.of_LessEqual_ne with both.left, both.right6768theorem LessEqual.cases (a b : Nat)69  requires below : a ≤ b70  shows a < b ∨ a = b71proof72  have split : a = b ∨ a ≠ b by tauto73  cases split with same | distinct74  . right75    exact same76  . left77    exact Less.of_LessEqual_ne with *7879theorem LessEqual.iff_Less_or_eq (a b : Nat)80  shows a ≤ b ↔ a < b ∨ a = b81proof82  constructor83  . intro below84    exact LessEqual.cases with below85  . intro split86    cases split with less | same87    . exact Less.implies_LessEqual with less88    . exact LessEqual.of_eq with same8990theorem LessEqual.not_Less (a b : Nat)91  requires below : a ≤ b92  shows ¬b < a93proof94  intro above95  have cycle := Less.transitive_LessEqual with above, below96  have excluded := Less.irreflexive at b97  exact excluded with cycle9899theorem Less.not_LessEqual (a b : Nat)100  requires below : a < b101  shows ¬b ≤ a102proof103  intro above104  have cycle := Less.transitive_LessEqual with below, above105  have excluded := Less.irreflexive at a106  exact excluded with cycle107108theorem Less.asymmetric (a b : Nat)109  requires below : a < b110  shows ¬b < a111proof112  exact LessEqual.not_Less with (Less.implies_LessEqual with below)113114theorem LessEqual.iff_not_Less (a b : Nat)115  shows a ≤ b ↔ ¬b < a116proof117  constructor118  . intro below119    exact LessEqual.not_Less with below120  . intro notAbove121    exact LessEqual.of_not_Less with notAbove122123theorem Less.iff_not_LessEqual (a b : Nat)124  shows a < b ↔ ¬b ≤ a125proof126  constructor127  . intro below128    exact Less.not_LessEqual with below129  . intro notAbove130    exact Less.of_not_LessEqual with notAbove131132theorem LessEqual.antisymmetric_iff (a b : Nat)133  shows a = b ↔ a ≤ b ∧ b ≤ a134proof135  constructor136  . intro same137    constructor138    . exact LessEqual.of_eq with same139    . symm at same140      exact LessEqual.of_eq with same141  . intro both142    exact LessEqual.antisymmetric with both.left, both.right143144theorem Less.or_LessEqual (a b : Nat)145  shows a < b ∨ b ≤ a146proof147  have split : a < b ∨ ¬a < b by tauto148  cases split with less | notLess149  . left150    exact less151  . right152    exact LessEqual.of_not_Less with notLess153154theorem Less.not_below_zero (a : Nat)155  shows ¬a < 0156proof157  intro below158  have zero : 0 ≤ a by linarith159  exact Less.not_LessEqual with below, zero160161theorem LessEqual.eq_zero (a : Nat)162  requires below : a ≤ 0163  shows a = 0164proof165  have zero : 0 ≤ a by linarith166  exact LessEqual.antisymmetric with below, zero167168theorem LessEqual.zero_iff (a : Nat)169  shows a ≤ 0 ↔ a = 0170proof171  constructor172  . intro below173    exact LessEqual.eq_zero with below174  . intro zero175    rw zero176    exact LessEqual.reflexive with *177178theorem Less.positive_of_ne_zero (a : Nat)179  requires nonzero : a ≠ 0180  shows 0 < a181proof182  have zero : 0 ≤ a by linarith183  have distinct : 0 ≠ a184    intro same185    symm at same186    exact nonzero with same187  exact Less.of_LessEqual_ne with zero, distinct188189theorem Less.ne_zero_of_positive (a : Nat)190  requires positive : 0 < a191  shows a ≠ 0192proof193  exact Less.ne_reverse with positive194195theorem Less.positive_iff (a : Nat)196  shows 0 < a ↔ a ≠ 0197proof198  constructor199  . intro positive200    exact Less.ne_zero_of_positive with positive201  . intro nonzero202    exact Less.positive_of_ne_zero with nonzero203204theorem LessEqual.one_of_positive (a : Nat)205  requires positive : 0 < a206  shows 1 ≤ a207proof208  linarith209210theorem LessEqual.one_iff_positive (a : Nat)211  shows 1 ≤ a ↔ 0 < a212proof213  constructor214  . intro one215    linarith216  . intro positive217    linarith218219theorem LessEqual.one_iff_ne_zero (a : Nat)220  shows 1 ≤ a ↔ a ≠ 0221proof222  constructor223  . intro one224    have positive : 0 < a by linarith225    exact Less.ne_zero_of_positive with positive226  . intro nonzero227    have positive := Less.positive_of_ne_zero with nonzero228    linarith229230theorem Less.zero_one231  shows 0 < 1232proof233  linarith234235theorem Less.add_one (a : Nat)236  shows a < a + 1237proof238  linarith239240theorem LessEqual.add_one (a : Nat)241  shows a ≤ a + 1242proof243  linarith244245theorem Less.add_one_iff (a b : Nat)246  shows a < b + 1 ↔ a ≤ b247proof248  constructor249  . intro below250    linarith251  . intro below252    linarith253254theorem LessEqual.add_one_iff (a b : Nat)255  shows a + 1 ≤ b + 1 ↔ a ≤ b256proof257  constructor258  . intro below259    linarith260  . intro below261    linarith262263theorem Less.add_one_both_iff (a b : Nat)264  shows a + 1 < b + 1 ↔ a < b265proof266  constructor267  . intro below268    linarith269  . intro below270    linarith271272theorem LessEqual.add_left_self (a k : Nat)273  shows a ≤ k + a274proof275  linarith276277theorem LessEqual.add_monotone_left (a b c : Nat)278  requires below : a ≤ b279  shows c + a ≤ c + b280proof281  linarith282283theorem LessEqual.add_right_iff (a b c : Nat)284  shows a + c ≤ b + c ↔ a ≤ b285proof286  constructor287  . intro below288    exact LessEqual.add_right_cancel with below289  . intro below290    linarith291292theorem LessEqual.add_left_iff (a b c : Nat)293  shows c + a ≤ c + b ↔ a ≤ b294proof295  constructor296  . intro below297    exact LessEqual.add_left_cancel with below298  . intro below299    linarith300301theorem Less.add_monotone_right (a b c : Nat)302  requires below : a < b303  shows a + c < b + c304proof305  linarith306307theorem Less.add_monotone_left (a b c : Nat)308  requires below : a < b309  shows c + a < c + b310proof311  linarith312313theorem Less.add_left_cancel (a b c : Nat)314  requires below : c + a < c + b315  shows a < b316proof317  linarith318319theorem Less.add_right_iff (a b c : Nat)320  shows a + c < b + c ↔ a < b321proof322  constructor323  . intro below324    linarith325  . intro below326    linarith327328theorem Less.add_left_iff (a b c : Nat)329  shows c + a < c + b ↔ a < b330proof331  constructor332  . intro below333    linarith334  . intro below335    linarith336337theorem LessEqual.of_add_left (a b c : Nat)338  requires below : a + b ≤ c339  shows a ≤ c340proof341  linarith342343theorem LessEqual.of_add_right (a b c : Nat)344  requires below : a + b ≤ c345  shows b ≤ c346proof347  linarith348349theorem Less.of_add_left (a b c : Nat)350  requires below : a + b < c351  shows a < c352proof353  linarith354355theorem Less.of_add_right (a b c : Nat)356  requires below : a + b < c357  shows b < c358proof359  linarith360361theorem Less.add_positive_left (a k : Nat)362  requires positive : 0 < k363  shows a < k + a364proof365  linarith366367theorem Less.add_positive_right (a k : Nat)368  requires positive : 0 < k369  shows a < a + k370proof371  linarith372373theorem LessEqual.double (a : Nat)374  shows a ≤ a + a375proof376  linarith377378theorem Less.double_of_positive (a : Nat)379  requires positive : 0 < a380  shows a < a + a381proof382  linarith383384theorem LessEqual.mul_right (a b k : Nat)385  requires below : a ≤ b386  shows a * k ≤ b * k387proof388  have left := LessEqual.mul_left at a, b, k with below389  have swapA := mul.commutative at a, k with *390  have swapB := mul.commutative at b, k with *391  rw [swapA, swapB] at left392  exact left393394theorem LessEqual.mul (a b c d : Nat)395  requires first : a ≤ b396  requires second : c ≤ d397  shows a * c ≤ b * d398proof399  have left := LessEqual.mul_right at a, b, c with first400  have right := LessEqual.mul_left at c, d, b with second401  exact LessEqual.transitive with left, right402403theorem Less.mul_right (a b k : Nat)404  requires positive : k ≠ 0405  requires below : a < b406  shows a * k < b * k407proof408  have left := Less.mul_left at a, b, k with positive, below409  have swapA := mul.commutative at a, k with *410  have swapB := mul.commutative at b, k with *411  rw [swapA, swapB] at left412  exact left413414theorem Less.mul (a b c d : Nat)415  requires first : a < b416  requires second : c < d417  shows a * c < b * d418proof419  have bPositive : b ≠ 0420    intro zero421    rw zero at first422    exact Less.not_below_zero with first423  have weak := Less.implies_LessEqual with first424  have left := LessEqual.mul_right at a, b, c with weak425  have right := Less.mul_left at c, d, b with bPositive, second426  exact LessEqual.transitive_Less with left, right427428theorem Less.mul_positive (a b : Nat)429  requires first : 0 < a430  requires second : 0 < b431  shows 0 < a * b432proof433  have aNonzero := Less.ne_zero_of_positive with first434  have bNonzero := Less.ne_zero_of_positive with second435  have nonzero := mul.nonzero with aNonzero, bNonzero436  exact Less.positive_of_ne_zero with nonzero437438theorem mul.positive_iff (a b : Nat)439  shows 0 < a * b ↔ 0 < a ∧ 0 < b440proof441  constructor442  . intro positive443    have nonzero := Less.ne_zero_of_positive with positive444    constructor445    . apply Less.positive_of_ne_zero446      intro zero447      rw zero at nonzero448      have vanish := mul.left_zero at b449      exact nonzero with vanish450    . apply Less.positive_of_ne_zero451      intro zero452      rw zero at nonzero453      have vanish := mul.right_zero at a454      exact nonzero with vanish455  . intro both456    exact Less.mul_positive with both.left, both.right457458theorem mul.eq_zero_iff (a b : Nat)459  shows a * b = 0 ↔ a = 0 ∨ b = 0460proof461  constructor462  . intro zero463    have split : a = 0 ∨ a ≠ 0 by tauto464    cases split with aZero | aNonzero465    . left466      exact aZero467    . right468      have factor := mul.eq_zero with zero469      cases factor with first | second470      . exfalso471        exact aNonzero with first472      . exact second473  . intro split474    cases split with aZero | bZero475    . rw aZero476      exact mul.left_zero with *477    . rw bZero478      exact mul.right_zero with *479480theorem LessEqual.mul_left_cancel_positive (a b k : Nat)481  requires positive : k ≠ 0482  requires below : k * a ≤ k * b483  shows a ≤ b484proof485  have split := Less.or_LessEqual at b, a486  cases split with above | fine487  . have strict := Less.mul_left at b, a, k with positive, above488    exfalso489    exact LessEqual.not_Less with below, strict490  . exact fine491492theorem LessEqual.mul_right_cancel_positive (a b k : Nat)493  requires positive : k ≠ 0494  requires below : a * k ≤ b * k495  shows a ≤ b496proof497  have swapA := mul.commutative at k, a with *498  have swapB := mul.commutative at k, b with *499  rw [swapA, swapB] at below500  exact LessEqual.mul_left_cancel_positive with positive, below501502theorem Less.mul_right_cancel_positive (a b k : Nat)503  requires positive : k ≠ 0504  requires below : a * k < b * k505  shows a < b506proof507  have swapA := mul.commutative at k, a with *508  have swapB := mul.commutative at k, b with *509  rw [swapA, swapB] at below510  exact Less.mul_left_cancel_positive with positive, below511512theorem LessEqual.le_mul_left (a k : Nat)513  requires positive : k ≠ 0514  shows a ≤ k * a515proof516  have one := LessEqual.one_iff_ne_zero.backward with positive517  have scaled := LessEqual.mul_right at 1, k, a with one518  have unit := mul.left_unit at a519  rw unit at scaled520  exact scaled521522theorem LessEqual.le_mul_right (a k : Nat)523  requires positive : k ≠ 0524  shows a ≤ a * k525proof526  have left := LessEqual.le_mul_left at a, k with positive527  have swap := mul.commutative at a, k with *528  rw swap at left529  exact left530531theorem LessEqual.one_le_mul (a b : Nat)532  requires first : 1 ≤ a533  requires second : 1 ≤ b534  shows 1 ≤ a * b535proof536  have product := LessEqual.mul with first, second537  have unit := mul.left_unit at 1538  rw unit at product539  exact product540541theorem LessEqual.mul_self (a : Nat)542  shows a ≤ a * a543proof544  have split : a = 0 ∨ a ≠ 0 by tauto545  cases split with zero | nonzero546  . rw zero547    linarith548  . exact LessEqual.le_mul_left with nonzero549550theorem mul.eq_one (a b : Nat)551  requires product : a * b = 1552  shows a = 1 ∧ b = 1553proof554  have aNonzero : a ≠ 0555    intro zero556    rw zero at product557    have vanish := mul.left_zero at b558    rw vanish at product559    have impossible : 0 < 0 by linarith560    exact Less.irreflexive with impossible561  have bNonzero : b ≠ 0562    intro zero563    rw zero at product564    have vanish := mul.right_zero at a565    rw vanish at product566    have impossible : 0 < 0 by linarith567    exact Less.irreflexive with impossible568  have aBound := LessEqual.le_mul_right at a, b with bNonzero569  have bBound := LessEqual.le_mul_left at b, a with aNonzero570  rw product at aBound571  rw product at bBound572  have aOne := LessEqual.one_iff_ne_zero.backward with aNonzero573  have bOne := LessEqual.one_iff_ne_zero.backward with bNonzero574  constructor575  . exact LessEqual.antisymmetric with aBound, aOne576  . exact LessEqual.antisymmetric with bBound, bOne577578theorem Less.one_lt_iff (a : Nat)579  shows 1 < a ↔ a ≠ 0 ∧ a ≠ 1580proof581  constructor582  . intro above583    constructor584    . intro zero585      rw zero at above586      exact Less.not_below_zero with above587    . exact Less.ne_reverse with above588  . intro both589    have one := LessEqual.one_iff_ne_zero.backward with both.left590    have distinct : 1 ≠ a591      intro same592      symm at same593      exact both.right with same594    exact Less.of_LessEqual_ne with one, distinct595596theorem Less.exists_add_one (a b : Nat)597  requires below : a < b598  shows ∃ k, Nat(k) ∧ b = a + k + 1599proof600  obtain ⟨k, kNat, equation⟩ := below601  witness k602  have shape : succ(a) + k = a + k + 1 by ring603  rw shape at equation604  symm605  exact equation606607theorem Less.add_one_le_of_lt (a b : Nat)608  requires below : a < b609  shows a + 1 ≤ b610proof611  linarith612613theorem Less.of_add_one_le (a b : Nat)614  requires below : a + 1 ≤ b615  shows a < b616proof617  linarith618619theorem Less.lt_of_lt_of_eq (a b c : Nat)620  requires below : a < b621  requires same : b = c622  shows a < c623proof624  rw ← same625  exact below626627theorem LessEqual.le_of_le_of_eq (a b c : Nat)628  requires below : a ≤ b629  requires same : b = c630  shows a ≤ c631proof632  rw ← same633  exact below634