WithBot

Statistics

Metric	Count
Definitions	0
Theorems `one_le_iff_pos`, `succ_natCast`, `succ_ofNat`, `succ_one`, `succ_zero`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`one_le_iff_pos` 📖	mathematical	—	`WithBot` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `one` `AddMonoidWithOne.toOne` `Preorder.toLT` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	—
`succ_natCast` 📖	mathematical	—	`succ` `SuccAddOrder.toSuccOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `WithBot` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`coe_natCast` `succ_coe` `Order.succ_eq_add_one`
`succ_ofNat` 📖	mathematical	—	`succ` `SuccAddOrder.toSuccOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne`	—	`succ_natCast`
`succ_one` 📖	mathematical	—	`succ` `SuccAddOrder.toSuccOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `WithBot` `one` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_one` `one_add_one_eq_two` `succ_natCast`
`succ_zero` 📖	mathematical	—	`succ` `SuccAddOrder.toSuccOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `WithBot` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Nat.cast_zero` `zero_add` `succ_natCast`

---