MIL/C05_Elementary_Number_Theory/solutions/Solutions_S04_More_Induction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
  1. def more_induction.fib line 7 source

    no axioms what this means

    Statement uses: Nat

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean:44 (same declaration text).

  2. theorem more_induction.fib_add_two line 12 source

    no axioms what this means

    Statement uses: Nat, Eq, more_induction.fib, HAdd.hAdd, OfNat.ofNat

    Proof uses: rfl

    6 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean:49 (same declaration text).

  3. theorem more_induction.fib_add line 14 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, more_induction.fib, HAdd.hAdd, OfNat.ofNat, HMul.hMul

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', add_zero, MulZeroClass.mul_zero, mul_one, zero_add, eq_self, Eq.mpr, id, Eq.mp, add_comm, add_assoc, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 19 more

    33 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean:92 (same declaration text).

    Tactic trace: 7 steps

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

  4. example more_induction.(example at line 23) line 23 source