MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. example C02S04.(example at line 13) line 13 source
  2. example C02S04.(example at line 20) line 20 source
  3. theorem C02S04.aux line 41 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, HAdd.hAdd, Min.min

    Proof uses: le_min, add_le_add_left, min_le_left, min_le_right

    17 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean:45 (same statement text; different proof or body). Qualify references as C02S04.aux@path.

    Tactic trace: 42 steps

    Open to load the checked before-and-after goal states.

  4. example C02S04.(example at line 48) line 48 source
  5. example C02S04.(example at line 59) line 59 source
  6. example C02S04.(example at line 69) line 69 source

    Source comment

    alternatively
    example : |a| - |b| ≤ |a - b| := by
…
  7. example C02S04.(example at line 79) line 79 source
  8. example C02S04.(example at line 82) line 82 source
  9. example C02S04.(example at line 86) line 86 source
  10. example C02S04.(example at line 89) line 89 source
  11. example C02S04.(example at line 109) line 109 source