[ add ] injectivity of `suc` for relation `m ≡ n (mod o)` for `{{NonZero o}}`#2971

Merged

MatthewDaggitt merged 15 commits intoagda:masterfrom

jamesmckinna:jacques-lemma

Apr 8, 2026

Commits on Mar 27, 2026

Commits on Mar 28, 2026

add: one half of the equivalence
jamesmckinna
committed

Commits on Mar 29, 2026

refactor: in terms of `_on_` and `_⇒_`; introduce name for equality mod `o`
jamesmckinna
committed

Commits on Mar 31, 2026

Commits on Apr 2, 2026

refactor: appeal to `Sum` elimination, rather than `with`
jamesmckinna
committed

Commits on Apr 8, 2026

Remove Zulip reference
MatthewDaggitt
authored