MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean

GitHub source file

13 declarations, 7 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example C02S04.(example at line 13) line 13 source
  2. example C02S04.(example at line 24) line 24 source
  3. example C02S04.(example at line 34) line 34 source
  4. example C02S04.(example at line 41) sorry line 41 source
  5. example C02S04.(example at line 43) sorry line 43 source
  6. theorem C02S04.aux sorry line 45 source

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    9 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 7 steps

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

  7. example C02S04.(example at line 47) sorry line 47 source
  8. example C02S04.(example at line 51) sorry line 51 source
  9. example C02S04.(example at line 58) line 58 source
  10. example C02S04.(example at line 61) line 61 source
  11. example C02S04.(example at line 65) line 65 source
  12. example C02S04.(example at line 68) sorry line 68 source
  13. example C02S04.(example at line 80) sorry line 80 source