NatFactorial

Statistics

Metric	Count
Definitions `evalNatAscFactorial`, `evalNatDescFactorial`, `evalNatFactorial`, `proveAscFactorial`	4
Theorems `asc_factorial_aux`, `isNat_ascFactorial`, `isNat_descFactorial`, `isNat_descFactorial_zero`, `isNat_factorial`	5
Total	9

Name	Kind	Assumes	Proves	Validates	Depends On
`asc_factorial_aux` 📖	—	`Nat.ascFactorial`	—	—	`Nat.ascFactorial_mul_ascFactorial`
`isNat_ascFactorial` 📖	—	`IsNat` `Nat.instAddMonoidWithOne` `Nat.ascFactorial`	—	—	`IsNat.out`
`isNat_descFactorial` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne` `Nat.ascFactorial`	`Nat.descFactorial`	—	`IsNat.out` `Nat.cast_add` `Nat.add_descFactorial_eq_ascFactorial`
`isNat_descFactorial_zero` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`Nat.descFactorial`	—	`IsNat.out` `Nat.cast_add` `Nat.cast_one` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `MulZeroClass.zero_mul` `Nat.cast_zero`
`isNat_factorial` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne` `Nat.ascFactorial`	`Nat.factorial`	—	`IsNat.out` `Nat.one_ascFactorial`

---