Proof that addition under modulo n is associative

add_mod_assoc.v

From Coq.Arith Require Import PeanoNat.
Import Nat.
Require Import Lia.

Definition add_mod n i j :=
  match i + j ?= n with
  | Lt => i + j
  | _ => i + j - n
  end.

Ltac solve_compare :=
  repeat match goal with
         | [ |- context [ match ?x ?= ?y with _ => _ end ] ] =>
           destruct (compare_spec x y); simpl; auto; try lia
         end.

Theorem add_mod_assoc n : 0 < n ->
  forall a b c, a < n -> b < n -> c < n -> add_mod n (add_mod n a b) c
                                 = add_mod n a (add_mod n b c).
Proof. intros; unfold add_mod; solve_compare. Qed.

Theorem add_mod_inverse n : 0 < n ->
  forall i, i < n -> add_mod n i (n - i) = 0.
Proof. intros; unfold add_mod; solve_compare. Qed.

Theorem add_mod_id n : 0 < n ->
  forall i, i < n -> add_mod n i 0 = i.
Proof. intros; unfold add_mod; solve_compare. Qed.