Commit 2023-07-10 13:59 5a78ace7

View on Github →

feat: port Init.Data.Nat.Lemmas (#5782) Previously this was an ad-hoc port

Estimated changes

modified def Nat.discriminate
modified theorem Nat.one_eq_succ_zero
added def Nat.subInduction
deleted def Nat.sub_induction