diff --git a/Util/Fin.v b/Util/Fin.v
index 079cac6ae9152eae863ad89ff6580940b91a90b3..65f0b6a4a43e4630f8e819d9a705954e18a1c960 100644
--- a/Util/Fin.v
+++ b/Util/Fin.v
@@ -274,12 +274,6 @@ Proof using .
   rewrite S_pred_ub. apply Nat.mod_same, neq_ub_0.
 Qed.
 
-Lemma mod2fin_comp : ∀ m1 m2 : nat, mod2fin (m1 + m2) = addm (mod2fin m1) m2.
-Proof using .
-  intros. apply fin2nat_inj. rewrite addm2nat, 2 mod2fin2nat,
-  Nat.add_mod_idemp_l. reflexivity. apply neq_ub_0.
-Qed.
-
 Definition addf (f1 f2 : fin ub) : fin ub := addm f1 f2.
 
 Definition addf_compat : Proper (equiv ==> equiv ==> equiv) addf := _.
@@ -342,6 +336,23 @@ Proof using .
   intros. rewrite addf_addm, mod2fin2nat, addm_mod. reflexivity.
 Qed.
 
+Definition divn (m : nat) : nat := m / ub.
+
+Lemma divnE : ∀ m : nat, divn m = m / ub.
+Proof using . reflexivity. Qed.
+
+Lemma addn_divn_mod2fin : ∀ m : nat, ub * divn m + mod2fin m = m.
+Proof using .
+  intros. symmetry. rewrite mod2fin2nat. apply Nat.div_mod, neq_ub_0.
+Qed.
+
+Lemma divn_mod2fin : ∀ m m' : nat,
+  mod2fin m = mod2fin m' -> divn m = divn m' -> m = m'.
+Proof using .
+  intros * Hm Hd. rewrite <- (addn_divn_mod2fin m), <- (addn_divn_mod2fin m'),
+  Hm, Hd. reflexivity.
+Qed.
+
 Lemma rev_fin_subproof : ∀ f : fin ub, Nat.pred ub - f < ub.
 Proof using .
   intros. eapply Nat.le_lt_trans. apply Nat.le_sub_l. apply lt_pred_ub.
@@ -657,7 +668,7 @@ Proof using . intros. rewrite 2 addm_addf. apply subf_addf_addf. Qed.
 Lemma subm_comp : ∀ (f : fin ub) (m2 m1 : nat),
   subm (subm f m1) m2 = subm f (m1 + m2).
 Proof using .
-  intros. rewrite 3 subm_subf, <- subf_addf, mod2fin_comp, addm_addf.
+  intros. rewrite 3 subm_subf, <- subf_addf, mod2fin_addm, addm_addf.
   reflexivity.
 Qed.
 
diff --git a/Util/NumberComplements.v b/Util/NumberComplements.v
index d9666fcdcf132aefe4a979b5df55fdc19d679566..60f83cfa6a0f51152a0121d5ec6215f0c0c2c2a9 100644
--- a/Util/NumberComplements.v
+++ b/Util/NumberComplements.v
@@ -273,6 +273,12 @@ Qed.
 
 Definition bounded_diff (n p m : nat) : Prop := p <= m < p + n.
 
+Lemma bounded_diff_neq_0 : ∀ n p m : nat, bounded_diff n p m -> n ≠ 0.
+Proof using .
+  intros * [H1 H2] Heq. subst. eapply (Nat.lt_irrefl p), Nat.le_lt_trans.
+  apply H1. rewrite <- (Nat.add_0_r p). apply H2.
+Qed.
+
 Lemma locally_bounded_diff : ∀ P : nat -> nat -> Prop, Symmetric P
   -> ∀ n : nat, (∀ m1 m2 : nat, m1 <= m2 -> m2 - m1 < n -> P m1 m2)
   <-> ∀ (p m1 m2: nat), bounded_diff n p m1 -> bounded_diff n p m2
@@ -295,12 +301,12 @@ Proof using .
   intros * a1 a2 H1 H2. symmetry. apply H1. symmetry. exact H2.
 Qed.
 
-Lemma mod_bounded_diff : ∀ p n m1 m2 : nat, bounded_diff (S n) p m1
-  -> bounded_diff (S n) p m2 -> m1 mod (S n) = m2 mod (S n) -> m1 = m2.
+Lemma mod_bounded_diff_inj : ∀ p n m1 m2 : nat, bounded_diff n p m1
+  -> bounded_diff n p m2 -> m1 mod n = m2 mod n -> m1 = m2.
 Proof using .
-  intros p n. eapply (locally_bounded_diff _ (inj_sym _ _ (eq_setoid nat)
-  (eq_setoid nat) (λ x, x mod (S n)))). intros * H1 H2 H3.
-  eapply mod_locally_inj. apply Nat.neq_succ_0. all: eassumption.
+  intros * H. pose proof (bounded_diff_neq_0 _ _ _ H) as Hn. revert m1 m2 H.
+  eapply (locally_bounded_diff _ (inj_sym _ _ (eq_setoid nat) (eq_setoid nat)
+  (λ x, x mod n))). intros * H1 H2 H3. eapply mod_locally_inj. all: eassumption.
 Qed.
 
 Lemma sub_sub : ∀ m n p : nat, p <= n → m - (n - p) = m + p - n.