proposition: Lemma mod_S_expand i n (NZ : n <> 0) : (S i mod n) = if eq_op n 1 then 0 else if eq_op (S (i mod n)) n then 0 else S (i mod n).
proof: Proof. desf; desf; rewrite Nat.add_mod with (a := 1); try done; rewrite (Nat.mod_small 1); try lia. by simpl; rewrite Heq0, Nat.mod_same. assert (UB := Nat.mod_upper_bound i n). rewrite (Nat.mod_small (1 + i mod n)); lia. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite