Zulip Chat Archive
Stream: new members
Topic: nats >= 0
bulut buyru (Mar 29 2019 at 00:40):
is there a way to easily prove that all nats are >= 0?
Mario Carneiro (Mar 29 2019 at 00:42):
nat.zero_le
bulut buyru (Mar 29 2019 at 01:31):
also, is there a tactic for strong induction?
Mario Carneiro (Mar 29 2019 at 01:34):
not a tactic, but you can write functions and theorems by well founded recursion, or you can apply nat.strong_induction_on
Last updated: May 02 2025 at 03:31 UTC