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.

def Mathlib.Tactic.PNatToNat.tacticPnat_positivity : Lean.ParserDescr

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

theorem Mathlib.Tactic.PNatToNat.coe_inj (m n : ℕ+) : m = n ↔ ↑m = ↑n

theorem Mathlib.Tactic.PNatToNat.coe_le_coe (m n : ℕ+) : m ≤ n ↔ ↑m ≤ ↑n

theorem Mathlib.Tactic.PNatToNat.coe_lt_coe (m n : ℕ+) : m < n ↔ ↑m < ↑n

theorem Mathlib.Tactic.PNatToNat.sub_coe (a b : ℕ+) : ↑(a - b) = ↑a - 1 - ↑b + 1

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; lia.