ParentFull threadscapp·Nothing wrong with starting at 1 for induction, but yes, having an additive monoid is nice (still get a multiplicative monoid with N*)View on HN