Commit 2022-11-17 12:36 5d138132

View on Github →

feat: port Data.PNat.Defs (#604) First attempt - I hope it's going in the right direction ported from 70fd9563a21e7b963887c9360bd29b2393e6225a (technically from an earlier commit, but it hasn't changed since)

Estimated changes

added theorem Nat.natPred_succPNat
added def Nat.succPNat
added theorem Nat.succPNat_coe
added def Nat.toPNat'
added theorem Nat.toPNat'_coe
added def Nat.toPNat
added theorem PNat.coe_eq_one_iff
added theorem PNat.coe_injective
added theorem PNat.coe_le_coe
added theorem PNat.coe_lt_coe
added theorem PNat.coe_toPNat'
added def PNat.div
added def PNat.divExact
added theorem PNat.div_coe
added theorem PNat.eq
added theorem PNat.mk_coe
added theorem PNat.mk_le_mk
added theorem PNat.mk_lt_mk
added theorem PNat.mk_one
added def PNat.mod
added def PNat.modDiv
added def PNat.modDivAux
added theorem PNat.mod_coe
added def PNat.natPred
added theorem PNat.natPred_eq_pred
added theorem PNat.ne_zero
added theorem PNat.not_lt_one
added theorem PNat.one_coe
added theorem PNat.one_le
added theorem PNat.pos
added theorem PNat.succPNat_natPred
added theorem PNat.toPNat'_coe
added def PNat