Commit 2022-11-21 04:21 112b847a

feat: mod_cases tactic (#593)

• depends on #587 Implements the mod_cases tactic, a teaching tactic used by @hrmacbeth 's class which is also generally useful.
• The tactic mod_cases h : e % 3 will perform a case disjunction on e : ℤ and yield subgoals containing the assumptions h : e ≡ 0 [ZMOD 3], h : e ≡ 1 [ZMOD 3], h : e ≡ 2 [ZMOD 3] respectively.
• In general, mod_cases h : e % n works when n is a positive numeral and e is an expression of type ℤ.
• If h is omitted as in mod_cases e % n, it will be default-named H.