Documentation

Mathlib.Tactic.PNatToNat

pnat_to_nat #

This file implements the pnat_to_nat tactic that shifts PNats in the context to Nat.

Implementation details #

The implementation follows these steps:

  1. For each x : PNat in the context, add the hypothesis 0 < (↑x : ℕ).
  2. Translate arithmetic on PNat to Nat using the pnat_to_nat_coe simp set.
source
def Mathlib.Tactic.PNatToNat.tacticPnat_positivity :
Lean.ParserDescr

For each x : PNat in the context, add the hypothesis 0 < (↑x : ℕ).

Equations
Instances For
    source
    theorem Mathlib.Tactic.PNatToNat.coe_inj (m n : ℕ+) :
    m = n ↔ ↑m = ↑n
    source
    theorem Mathlib.Tactic.PNatToNat.coe_le_coe (m n : ℕ+) :
    m ≤ n ↔ ↑m ≤ ↑n
    source
    theorem Mathlib.Tactic.PNatToNat.coe_lt_coe (m n : ℕ+) :
    m < n ↔ ↑m < ↑n
    source
    theorem Mathlib.Tactic.PNatToNat.sub_coe (a b : ℕ+) :
    ↑(a - b) = ↑a - 1 - ↑b + 1
    source
    def Mathlib.Tactic.PNatToNat.tacticPnat_to_nat :
    Lean.ParserDescr

    pnat_to_nat shifts all PNats in the context to Nat, rewriting propositions about them. A typical use case is pnat_to_nat; omega.

    Equations
    Instances For