Order related instances for ℕ+

instance PNat.instSuccOrder : SuccOrder ℕ+

Equations

• PNat.instSuccOrder = SuccOrder.ofSuccLeIff (fun (x : ℕ+) => x + 1) @PNat.instSuccOrder._proof_2

instance PNat.instSuccAddOrder : SuccAddOrder ℕ+

Equations

• PNat.instSuccAddOrder = { toSuccOrder := PNat.instSuccOrder, succ_eq_add_one := PNat.instSuccAddOrder._proof_1 }

instance PNat.instNoMaxOrder : NoMaxOrder ℕ+

@[simp]

theorem PNat.succ_eq_add_one (n : ℕ+) : Order.succ n = n + 1