diff --git a/CaseStudies/Convergence/Algorithm_noB.v b/CaseStudies/Convergence/Algorithm_noB.v
index b25e7cb5da58a39643e4071ce17cebb28ed3494a..f347a298a879ab5e551f668edaf4a5fec426665e 100644
--- a/CaseStudies/Convergence/Algorithm_noB.v
+++ b/CaseStudies/Convergence/Algorithm_noB.v
@@ -30,10 +30,10 @@ Typeclasses eauto := (bfs).
 
 
 Section ConvergenceAlgo.
-(** There are [n] good robots and no byzantine one. *)
-Variable n : nat.
+(** There are [ub] good robots and no byzantine one. *)
+Context {gt0 : greater_than 0}.
 
-Instance MyRobots : Names := Robots (S n) 0.
+Instance MyRobots : Names := Robots ub 0.
 Instance NoByz : NoByzantine.
 Proof using . now split. Qed.
 
diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index 91351b25a2a5c36aa044454b9b4229c8613984eb..6eab56689e61b511490ba6f995f4b15f9d95c7a3 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -17,26 +17,28 @@ Typeclasses eauto := (bfs).
 Section Exploration.
 
 (** Given an abitrary ring *)
-Context {RR : RingSpec}.
-(** There are kG good robots and no byzantine ones. *)
-Variable k : nat.
-Instance Robots : Names := Robots (S k) 0.
+Context {gt2 : greater_than 2}.
+(** There are k good robots and no byzantine ones. *)
+Context {gt0 : greater_than 0}.
+Notation n := (@ub 2 gt2).
+Notation k := (@ub 0 gt0).
+Instance Robots : Names := Robots k 0.
 
 (** Assumptions on the number of robots: it strictly divides the ring size. *)
-Hypothesis kdn : (S (S (S n)) mod (S k) = 0).
-Hypothesis k_inf_n : (S k < S (S (S n))).
+Hypothesis kdn : (n mod k = 0).
+Hypothesis k_inf_n : (k < n).
 
-Lemma local_subproof1 : S (S (S n)) = S k * (S (S (S n)) / (S k)).
-Proof using kdn. apply Nat.div_exact. apply Nat.neq_succ_0. apply kdn. Qed.
+Lemma local_subproof1 : n = k * (n / k).
+Proof using kdn. apply Nat.div_exact. apply neq_ub_lb. apply kdn. Qed.
 
-Lemma local_subproof2 : S (S (S n)) / (S k) ≠ 0.
+Lemma local_subproof2 : n / k ≠ 0.
 Proof using kdn.
-  intros Habs. elim (Nat.neq_succ_0 (S (S n))). rewrite local_subproof1, Habs.
+  intros Habs. eapply (@neq_ub_0 2 gt2). rewrite local_subproof1, Habs.
   apply Nat.mul_0_r.
 Qed.
 
 Lemma local_subproof3 : ∀ m : nat,
-  m < S k -> m * (S (S (S n)) / (S k)) < S (S (S n)).
+  m < k -> m * (n / k) < n.
 Proof using kdn.
   intros * H. rewrite local_subproof1 at 2. apply mult_lt_compat_r.
   apply H. apply Nat.neq_0_lt_0, local_subproof2.
@@ -62,7 +64,7 @@ Variable r : robogram.
 (** ***  Definition of the demon used in the proof  **)
 
 Definition create_ref_config (g : G) : location :=
-  mod2fin (fin2nat g * (S (S (S n)) / (S k))).
+  mod2fin (fin2nat g * (n / k)).
 
 (** The starting configuration where robots are evenly spaced:
     each robot is at a distance of [ring_size / kG] from the previous one,
@@ -83,7 +85,7 @@ Proof using kdn.
   all: apply local_subproof3, fin_lt.
 Qed.
 
-(**  Translating [ref_config] by multiples of [S (S (S n)) / (S k)]
+(**  Translating [ref_config] by multiples of [n / k]
      does not change its observation. *)
 Lemma obs_asbf_ref_config : forall g,
   !! (map_config (asbf (create_ref_config g)⁻¹) ref_config) == !! ref_config.
@@ -101,17 +103,17 @@ Proof using kdn.
     + rewrite NoDupA_Leibniz. apply names_NoDup.
   * intro pt. repeat rewrite InA_map_iff; autoclass; [].
     split; intros [id [Hpt _]]; revert Hpt; apply (no_byz id); clear id; intros g' Hpt.
-    + pose (id' := subf g' g). change (fin (S k)) with G in id'.
+    + pose (id' := subf g' g). change (fin k) with G in id'.
       exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
       rewrite <- Hpt. cbn-[subf create_ref_config]. split. 2: reflexivity.
       unfold create_ref_config, Datatypes.id, id'. apply fin2nat_inj.
       rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l,
       2 (Nat.mod_small (_ * _)). rewrite local_subproof1 at 3 5.
       rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r,
-      Nat.mul_mod_distr_r. reflexivity. 1,5: apply Nat.neq_succ_0.
+      Nat.mul_mod_distr_r. reflexivity. 1,5: apply neq_ub_0.
       apply local_subproof2. all: apply local_subproof3. apply fin_lt.
       apply mod2fin_lt.
-    + pose (id' := addf g' g). change (fin (S k)) with G in id'.
+    + pose (id' := addf g' g). change (fin k) with G in id'.
       exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
       rewrite <- Hpt. cbn. split. 2: reflexivity. unfold create_ref_config, id'.
       apply fin2nat_inj. rewrite subf2nat, 3 mod2fin2nat, addf2nat,
@@ -121,7 +123,7 @@ Proof using kdn.
       all: cycle 1. rewrite Nat.add_mod_idemp_l, <- Nat.add_assoc,
       le_plus_minus_r, <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r.
       apply Nat.mod_small. 4: apply Nat.lt_le_incl.
-      2,3,5,6,10: apply Nat.neq_succ_0. 3,6: apply local_subproof2.
+      2,3,5,6,10: apply neq_ub_0. 3,6: apply local_subproof2.
       3,4: apply local_subproof3. all: apply fin_lt.
 Qed.
 
@@ -181,12 +183,13 @@ Proof using Hmove kdn k_inf_n.
   intros e Heq_e. exists (mod2fin 1). intro Hl.
   induction Hl as [e [g Hvisited] | e Hlater IHvisited].
   * rewrite Heq_e in Hvisited. cbn in Hvisited.
-    apply (f_equal (@fin2nat (S (S (S n))))) in Hvisited. revert Hvisited.
+    apply (f_equal (@fin2nat n)) in Hvisited. revert Hvisited.
     cbn-[Nat.modulo Nat.div]. rewrite local_subproof1 at 2.
     rewrite Nat.mul_mod_distr_r, (Nat.mod_small 1), Nat.mul_eq_1.
     intros [_ Habs]. elim (lt_not_le _ _ k_inf_n). rewrite local_subproof1,
-    Habs, Nat.mul_1_r. reflexivity. 3: apply local_subproof2. apply lt_n_S,
-    Nat.neq_0_lt_0. all: apply Nat.neq_succ_0.
+    Habs, Nat.mul_1_r. reflexivity. 3: apply local_subproof2.
+    2: apply neq_ub_lb. erewrite <- smaller_bound_ub. apply lt_lb_ub.
+    Unshelve. auto.
   * apply IHvisited. rewrite Heq_e, execute_tail. rewrite round_id. f_equiv.
 Qed.
 
@@ -242,15 +245,15 @@ Qed.
 
 Lemma f_config_injective_N : ∀ config m1 m2,
   f_config config m1 == f_config config m2
-  -> m1 mod (S (S (S n))) == m2 mod (S (S (S n))).
+  -> m1 mod n == m2 mod n.
 Proof using kdn k_inf_n.
   unfold f_config. intros * Heq. specialize (Heq (Good fin0)).
-  unshelve eapply addm_bounded_diff_inj. 6: rewrite 2 addm_mod. 5: apply Heq.
-  2,3: split. 2,4: apply Nat.le_0_l. all: apply mod2fin_lt.
+  unshelve eapply (@addm_bounded_diff_inj 2 gt2). 5: rewrite 2 addm_mod.
+  5: apply Heq. 2,3: split. 2,4: apply Nat.le_0_l. all: apply mod2fin_lt.
 Qed.
 
 Lemma f_config_modulo : ∀ config m,
-  f_config config (m mod (S (S (S n)))) == f_config config m.
+  f_config config (m mod n) == f_config config m.
 Proof using . intros * id. apply addm_mod. Qed.
 
 Lemma asbf_f_config : ∀ (config : configuration) (id1 id2 : ident) (m : nat),
@@ -268,11 +271,11 @@ Definition equiv_config config1 config2 : Prop
 
 Lemma equiv_config_m_sym : ∀ m config1 config2,
   equiv_config_m m config1 config2
-  -> equiv_config_m (@oppm (S (S n)) m) config2 config1.
+  -> equiv_config_m (@oppm 2 gt2 m) config2 config1.
 Proof using k_inf_n kdn.
   unfold equiv_config_m. intros * Hequiv. unshelve erewrite Hequiv,
   f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _)).
-  apply Nat.neq_succ_0. symmetry. apply f_config_0. apply oppm_divide.
+  apply neq_ub_0. symmetry. apply f_config_0. apply oppm_divide.
 Qed.
 
 Lemma equiv_config_m_trans : ∀ m1 m2 config1 config2 config3,
@@ -286,14 +289,14 @@ Qed.
 Instance equiv_config_equiv : Equivalence equiv_config.
 Proof using k_inf_n kdn. split.
   + intro config. exists 0. unfold equiv_config_m. now rewrite f_config_0.
-  + intros config1 config2 [m Hm]. exists (@oppm (S (S n)) m).
+  + intros config1 config2 [m Hm]. exists (@oppm 2 gt2 m).
     apply (equiv_config_m_sym Hm).
   + intros ? ? ? [m1 Hm1] [m2 Hm2]. exists (m1 + m2).
     revert Hm1 Hm2. apply equiv_config_m_trans.
 Qed.
 
 Lemma equiv_config_mod : ∀ (m : nat) (config1 config2 : configuration),
-  equiv_config_m (m mod (S (S (S n)))) config1 config2
+  equiv_config_m (m mod n) config1 config2
   <-> equiv_config_m m config1 config2.
 Proof using .
   intros. split; intros H id.
@@ -351,7 +354,7 @@ Proof using .
 Qed.
 
 Lemma AlwaysEquiv_sym : ∀ m (e1 e2 : execution),
-  AlwaysEquiv m e1 e2 -> AlwaysEquiv (@oppm (S (S n)) m) e2 e1.
+  AlwaysEquiv m e1 e2 -> AlwaysEquiv (@oppm 2 gt2 m) e2 e1.
 Proof using k_inf_n kdn.
   cofix Hcoind. intros m1 e1 e2 [Hnow Hlater]. constructor.
   + now apply equiv_config_m_sym.
@@ -374,7 +377,7 @@ Proof using k_inf_n kdn.
 Qed.
 
 Lemma AlwaysEquiv_mod : ∀ (m : nat) (e1 e2 : execution),
-  AlwaysEquiv (m mod (S (S (S n)))) e1 e2 <-> AlwaysEquiv m e1 e2.
+  AlwaysEquiv (m mod n) e1 e2 <-> AlwaysEquiv m e1 e2.
 Proof using .
   intros. split.
   - revert m e1 e2. cofix Hrec. intros * H. constructor.
@@ -476,15 +479,15 @@ Qed.
 Lemma ref_config_AlwaysMoving : AlwaysMoving (execute r bad_demon ref_config).
 Proof using Hmove k_inf_n kdn.
   generalize (AlwaysEquiv_refl (execute r bad_demon ref_config)).
-  generalize 0, (execute r bad_demon ref_config) at 1 3.
-  cofix Hcoind. intros m e Hequiv. constructor.
+  generalize 0 at 1. generalize (execute r bad_demon ref_config) at 1 3. 
+  cofix Hcoind. intros e m Hequiv. constructor.
   + clear Hcoind. rewrite Hequiv. intros [Hstop _]. elim Hmove.
     unfold Stall in Hstop. rewrite execute_tail, round_simplify in Hstop.
-    simpl hd in Hstop. eapply move_along_I. rewrite move_along_0.
+    simpl hd in Hstop. apply (move_along_I fin0). rewrite move_along_0.
     apply fin2nat_inj. setoid_rewrite <- Nat.mod_small. 2,3: apply fin_lt.
     eapply f_config_injective_N. rewrite fin02nat, f_config_0.
     symmetry. apply Hstop.
-  + apply (Hcoind (addm (oppf target) m)). clear Hcoind. rewrite addm2nat,
+  + eapply (Hcoind _ (addm (oppf target) m)). clear Hcoind. rewrite addm2nat,
     Nat.add_comm. apply AlwaysEquiv_mod.
     apply AlwaysEquiv_trans with (tl (execute r bad_demon ref_config)).
     apply Hequiv. rewrite oppf_oppm.
diff --git a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
index c01e2d6574a49003c4bba6f7505f158ab1170b39..1d8c189bbec500f6ae8ccf3c9dd0bcb1ac3c594e 100644
--- a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
+++ b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
@@ -42,10 +42,10 @@ Typeclasses eauto := (bfs) 10.
 (** **  Framework of the correctness proof: a finite set with at least two elements  **)
 Section GatheringInR2.
 
-Variable n : nat.
+Context {gt1 : greater_than 1}.
 
 (** There are n good robots and no byzantine ones. *)
-Instance MyRobots : Names := Robots (S (S n)) 0.
+Instance MyRobots : Names := Robots ub 0.
 Instance NoByz : NoByzantine.
 Proof using . now split. Qed.
 
diff --git a/CaseStudies/Gathering/InR2/Viglietta.v b/CaseStudies/Gathering/InR2/Viglietta.v
index 8cddb92d27bb58b55d16529e998cda6ff53a1cce..2edb11fc430b66e2adf389a01a77ec66a5776325 100644
--- a/CaseStudies/Gathering/InR2/Viglietta.v
+++ b/CaseStudies/Gathering/InR2/Viglietta.v
@@ -34,8 +34,9 @@ Instance NoByz : NoByzantine.
 Proof using . now split. Qed.
 
 Notation lt2 := (fun x => x < 2)%nat.
+Definition lt02 : (0 < 2)%nat := ltac:(abstract auto).
 Definition lt12 : (1 < 2)%nat := ltac:(abstract lia).
-Definition r0 : G := fin0.
+Definition r0 : G := Fin lt02.
 Definition r1 : G := Fin lt12.
 
 Lemma id_case : forall id, id = Good r0 \/ id = Good r1.
diff --git a/Models/RingSSync.v b/Models/RingSSync.v
index 8eec2e0fee0cfe15851cd7e83fa54518e354a4ae..b262f29d963869e6a0479c428d1f5c6c67b006cf 100644
--- a/Models/RingSSync.v
+++ b/Models/RingSSync.v
@@ -6,7 +6,7 @@ Set Implicit Arguments.
 
 Section RingSSync.
 
-Context {RR : RingSpec} {Robots : Names}.
+Context {gt2 : greater_than 2} {Robots : Names}.
 
 Global Existing Instance NodesLoc.
 
diff --git a/Spaces/Graph.v b/Spaces/Graph.v
index 46c1253ef78ab180a9a74352bad4cd34040a24fe..a3227694ae56eec46100c75d202768e4175b777a 100644
--- a/Spaces/Graph.v
+++ b/Spaces/Graph.v
@@ -8,7 +8,6 @@
                                                                           *)
 (**************************************************************************)
 
-
 Require Import Rbase SetoidDec.
 From Pactole Require Import Util.Coqlib Util.Fin Core.State.
 Set Implicit Arguments.
diff --git a/Spaces/Ring.v b/Spaces/Ring.v
index 47c9e0add06b25f994f4f98f1df17e9de6f02fa1..40c0222f986ab884830228bdd22104cf2ca37f3a 100644
--- a/Spaces/Ring.v
+++ b/Spaces/Ring.v
@@ -14,14 +14,11 @@ From Pactole Require Import Util.Coqlib Util.Bijection Spaces.Graph
 
 (** ** A ring  **)
 
-(** What we need to define a ring. *)
-Class RingSpec := { n : nat }.
-
 Section Ring.
 
-Context {RR : RingSpec}.
+Context {gt2 : greater_than 2}.
 
-Definition ring_node := finite_node (S (S (S n))).
+Definition ring_node := finite_node ub.
 Inductive direction := Forward | Backward | SelfLoop.
 Definition ring_edge := (ring_node * direction)%type.
 
@@ -43,7 +40,7 @@ Definition dir2nat (d : direction) : nat :=
   match d with
     | SelfLoop => 0
     | Forward => 1
-    | Backward => S (S n)
+    | Backward => Nat.pred ub
   end.
 
 Definition dir2nat_compat : Proper (equiv ==> equiv) dir2nat := _.
@@ -54,19 +51,24 @@ Proof using . reflexivity. Qed.
 Lemma dir21 : dir2nat Forward = 1.
 Proof using . reflexivity. Qed.
 
-Lemma dir2SSn : dir2nat Backward = S (S n).
+Lemma dir2SSn : dir2nat Backward = Nat.pred ub.
 Proof using . reflexivity. Qed.
 
-Lemma dir2nat_lt : ∀ d : direction, dir2nat d < S (S (S n)).
-Proof using . intros. destruct d. all: cbn. all: lia. Qed.
+Lemma dir2nat_lt : ∀ d : direction, dir2nat d < ub.
+Proof using .
+  intros. destruct d. all: cbn. 2: apply lt_pred_ub.
+  all: apply lt_sb_ub. all: auto.
+Qed.
 
 Lemma dir2nat_inj : Util.Preliminary.injective equiv equiv dir2nat.
 Proof using .
-  intros d1 d2 H. destruct d1, d2. all: try inversion H. all: reflexivity.
+  intros d1 d2 H'. destruct d1, d2. all: inversion H' as [H].
+  all: try reflexivity. all: exfalso. 1,4: symmetry in H.
+  all: eapply neq_pred_ub_sb. 2,4,6,8: exact H. all: auto.
 Qed.
 
 Lemma dir2mod2fin : ∀ d : direction,
-  fin2nat (@mod2fin (S (S n)) (dir2nat d)) = dir2nat d.
+  fin2nat (mod2fin (dir2nat d)) = dir2nat d.
 Proof using .
   intros. rewrite mod2fin2nat. apply Nat.mod_small. apply dir2nat_lt.
 Qed.
@@ -76,7 +78,7 @@ Definition nat2Odir (m : nat) : option direction :=
   match m with
     | 0 => Some SelfLoop
     | 1 => Some Forward
-    | _ => if m =? S (S n) then Some Backward else None
+    | _ => if m =? Nat.pred ub then Some Backward else None
   end.
 
 Definition nat2Odir_compat : Proper (equiv ==> equiv) nat2Odir := _.
@@ -85,9 +87,11 @@ Lemma nat2Odir_Some : ∀ (d : direction) (m : nat),
   nat2Odir m = Some d <-> dir2nat d = m.
 Proof using .
   unfold dir2nat, nat2Odir. intros d m. split; intros H.
-  all: destruct d, m as [|p]. all: try inversion H. 6: rewrite Nat.eqb_refl.
-  all: try reflexivity. all: destruct p. all: try inversion H.
-  all: try reflexivity. all: destruct (S (S p) =? S (S n)) eqn:Hd.
+  all: destruct d, m as [|p]. all: try inversion H. all: try reflexivity.
+  4:{ exfalso. eapply neq_pred_ub_sb. 2: exact H. auto. }
+  4: rewrite Nat.eqb_refl. all: destruct p. all: try inversion H.
+  all: try reflexivity. 4:{ exfalso. eapply neq_pred_ub_sb. 2: exact H.
+  auto. } all: destruct (S (S p) =? Nat.pred ub) eqn:Hd.
   all: try inversion H. symmetry. apply Nat.eqb_eq, Hd.
 Qed.
 
@@ -106,7 +110,7 @@ Lemma nat2Odir_pick : ∀ m : nat,
 Proof using .
   intros. unfold nat2Odir. destruct m as [|m]. apply Pick, dir20.
   destruct m as [|m]. apply Pick, dir21.
-  destruct (S (S m) =? S (S n)) eqn:Hd.
+  destruct (S (S m) =? Nat.pred ub) eqn:Hd.
   - apply Nat.eqb_eq in Hd. rewrite Hd. apply Pick, dir2SSn.
   - apply Nat.eqb_neq in Hd. apply Nopick. intros d H. elim Hd.
     destruct d. all: inversion H. subst. reflexivity.
@@ -143,7 +147,7 @@ Lemma move_alongE : ∀ (v : ring_node) (d : direction),
 Proof using . intros. reflexivity. Qed.
 
 Definition move_along2nat : ∀ (v : ring_node) (d : direction),
-  fin2nat (move_along v d) = (v + dir2nat d) mod (S (S (S n))).
+  fin2nat (move_along v d) = (v + dir2nat d) mod ub.
 Proof using . intros. apply addm2nat. Qed.
 
 Lemma move_alongI_ : ∀ d : direction,
@@ -224,13 +228,13 @@ Definition swap_direction_bij : bijection direction
                       swap_directionK swap_directionK.
 
 Lemma dir2nat_swap_direction : ∀ d : direction,
-  dir2nat (swap_direction d) = @oppm (S (S n)) (dir2nat d).
+  dir2nat (swap_direction d) = oppm (dir2nat d).
 Proof using .
   intros. rewrite oppm_oppf, oppf2nat, dir2mod2fin. symmetry. destruct d.
-  2: cbn-[Nat.modulo Nat.sub]. 1,3: cbn-[Nat.modulo]. apply Nat.mod_small,
-  Nat.lt_succ_diag_r. apply Nat.mod_same, Nat.neq_succ_0.
-  rewrite 2 Nat.sub_succ, Nat.sub_succ_l, Nat.sub_diag. 2: reflexivity.
-  apply Nat.mod_small, lt_n_S, Nat.lt_0_succ.
+  2: cbn-[Nat.modulo Nat.sub]. 1,3: cbn-[Nat.modulo]. rewrite Nat.sub_1_r.
+  apply Nat.mod_small, lt_pred_ub. rewrite Nat.sub_0_r. apply Nat.mod_same,
+  neq_ub_0. rewrite <- S_pred_ub at 1. rewrite Nat.sub_succ_l,
+  Nat.sub_diag. apply Nat.mod_small. apply lt_sb_ub. auto. reflexivity.
 Qed.
 
 Lemma move_along_swap_direction : ∀ (v : ring_node) (d : direction),
@@ -324,10 +328,10 @@ Qed.
 Definition Ring (thd : ring_edge -> R)
                 (thd_pos : ∀ e, (0 < thd e < 1)%R)
                 (thd_compat : Proper (equiv ==> eq) thd)
-  : FiniteGraph (S (S (S n))) ring_edge.
+  : FiniteGraph ub ring_edge.
 Proof using .
   refine {|
-    V_EqDec := @finite_node_EqDec (S (S (S n)));
+    V_EqDec := @finite_node_EqDec ub;
     E_EqDec := ring_edge_EqDec;
     src := fst;
     tgt := λ e, move_along (fst e) (snd e);
@@ -341,7 +345,7 @@ Proof using .
 Defined.
 
 (** If we do not care about threshold values, we just take 1/2 everywhere. *)
-Global Instance nothresholdRing : FiniteGraph (S (S (S n))) ring_edge :=
+Global Instance nothresholdRing : FiniteGraph ub ring_edge :=
   Ring (fun _ => 1/2)%R
        ltac:(abstract (intro; lra))
        (fun _ _ _ => eq_refl).
@@ -354,7 +358,7 @@ Global Instance Ring_isomorphism_Setoid :
 Global Instance Ring_isomorphism_Inverse : Inverse (isomorphism nothresholdRing)
   := @IsoInverse _ _ nothresholdRing.
 
-Global Instance Ring_isomorphism_Compoosition
+Global Instance Ring_isomorphism_Composition
   : Composition (isomorphism nothresholdRing)
   := @IsoComposition _ _ nothresholdRing.
 
@@ -382,14 +386,14 @@ Defined.
 Definition trans_compat : Proper (equiv ==> equiv) trans := _.
 
 Lemma trans2nat : ∀ (m : nat) (v : ring_node), fin2nat (trans m v)
-  = (v + (S (S (S n)) - m mod (S (S (S n))))) mod (S (S (S n))).
+  = (v + (ub - m mod ub)) mod ub.
 Proof using . apply asbmV2nat. Qed.
 
 Lemma transV2nat : ∀ (m : nat) (v : ring_node),
-  fin2nat ((trans m)⁻¹ v) = (v + m) mod (S (S (S n))).
+  fin2nat ((trans m)⁻¹ v) = (v + m) mod ub.
 Proof using . apply asbm2nat. Qed.
 
-Lemma trans_mod : ∀ m : nat, trans (m mod (S (S (S n)))) == trans m.
+Lemma trans_mod : ∀ m : nat, trans (m mod ub) == trans m.
 Proof using .
   intros. split; [|split]. all: unfold trans.
   all: cbn-[equiv inverse Nat.modulo]. 1,2: rewrite asbm_mod.
@@ -416,30 +420,30 @@ Lemma transI_fin_max : (trans 1)⁻¹ fin_max = fin0.
 Proof using . apply asbm_fin_max. Qed.
 
 Lemma transI_fin0_divide : ∀ (v : ring_node) (m : nat),
-  Nat.divide (S (S (S n))) (v + m) ↔ (trans m)⁻¹ v = fin0.
+  Nat.divide ub (v + m) ↔ (trans m)⁻¹ v = fin0.
 Proof using . apply asbm_fin0_divide. Qed.
 
 Lemma trans_locally_inj : ∀ (m1 m2 : nat),
-  m1 ≤ m2 → m2 - m1 < S (S (S n)) → trans m1 == trans m2 → m1 = m2.
+  m1 ≤ m2 → m2 - m1 < ub → trans m1 == trans m2 → m1 = m2.
 Proof using .
   intros * ?? H. eapply asbmV_locally_inj. 3: apply H. all: eassumption.
 Qed.
 
 Lemma transV_locally_inj : ∀ (m1 m2 : nat),
-  m1 ≤ m2 → m2 - m1 < S (S (S n)) → (trans m1)⁻¹ == (trans m2)⁻¹ → m1 = m2.
+  m1 ≤ m2 → m2 - m1 < ub → (trans m1)⁻¹ == (trans m2)⁻¹ → m1 = m2.
 Proof using .
   intros * ?? H. eapply asbm_locally_inj. 3: apply H. all: eassumption.
 Qed.
 
 Lemma trans_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
-  bounded_diff (S (S (S n))) p m1 → bounded_diff (S (S (S n))) p m2
+  bounded_diff ub p m1 → bounded_diff ub p m2
   → trans m1 == trans m2 → m1 = m2.
 Proof using .
   intros * ?? H. eapply asbmV_bounded_diff_inj. 3: apply H. all: eassumption.
 Qed.
 
 Lemma transV_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
-  bounded_diff (S (S (S n))) p m1 → bounded_diff (S (S (S n))) p m2
+  bounded_diff ub p m1 → bounded_diff ub p m2
   → (trans m1)⁻¹ == (trans m2)⁻¹ → m1 = m2.
 Proof using .
   intros * ?? H. eapply asbm_bounded_diff_inj. 3: apply H. all: eassumption.
diff --git a/Util/Fin.v b/Util/Fin.v
index 920a71f8e664cee4db246e48b4e03e773743967f..42c9ab8f2342a79fe4a1bbab7faeafef1742f4f1 100644
--- a/Util/Fin.v
+++ b/Util/Fin.v
@@ -7,9 +7,9 @@ Unset Printing Implicit Defensive.
 
 Section Fin.
 
-Context (n : nat).
+Context (ub : nat).
 
-Inductive fin : Type :=  Fin : ∀ m : nat, m < n -> fin.
+Inductive fin : Type :=  Fin : ∀ m : nat, m < ub -> fin.
 
 Global Instance fin_Setoid : Setoid fin := eq_setoid fin.
 
@@ -26,9 +26,12 @@ Global Coercion fin2nat (f : fin) : nat := match f with @Fin m _ => m end.
 
 Definition fin2nat_compat : Proper (equiv ==> equiv) fin2nat := _.
 
-Lemma fin_lt : ∀ f : fin, f < n.
+Lemma fin_lt : ∀ f : fin, f < ub.
 Proof using . intros. destruct f as [m p]. exact p. Qed.
 
+Lemma fin_le : ∀ f : fin, f <= Nat.pred ub.
+Proof using . intros. apply Nat.lt_le_pred, fin_lt. Qed.
+
 Lemma fin2nat_inj : Preliminary.injective equiv equiv fin2nat.
 Proof using .
   intros [m1 H1] [m2 H2] Heq. cbn in Heq. subst. cbn. f_equal. apply le_unique.
@@ -36,83 +39,150 @@ Qed.
 
 End Fin.
 
+Class greater_than (lb : nat) := {
+  ub : nat;
+  lt_lb_ub : lb < ub;
+}.
+
+Section greater_than.
+
+Context {lb : nat} {gtlb : greater_than lb}.
+
+Lemma neq_ub_lb : ub ≠ lb.
+Proof using gtlb.
+  intros * H. apply (lt_irrefl lb). rewrite <- H at 2. exact lt_lb_ub.
+Qed.
+
+Lemma le_lb_pred_ub : lb <= Nat.pred ub.
+Proof using gtlb. intros. apply Nat.lt_le_pred, lt_lb_ub. Qed.
+
+Lemma lt_pred_ub : Nat.pred ub < ub.
+Proof using gtlb.
+  intros. eapply lt_pred_n_n, Nat.le_lt_trans. apply Nat.le_0_l. apply lt_lb_ub.
+Qed.
+
+Lemma S_pred_ub : S (Nat.pred ub) = ub.
+Proof using gtlb. intros. eapply Nat.lt_succ_pred, lt_lb_ub. Qed.
+
+Lemma lt_sb_ub : ∀ sb : nat, sb < lb -> sb < ub.
+Proof using gtlb. intros * H. eapply Nat.lt_trans. exact H. exact lt_lb_ub. Qed.
+
+Lemma lt_sb_pred_ub : ∀ sb : nat, sb < lb -> sb < Nat.pred ub.
+Proof using gtlb.
+  intros * H. eapply Nat.lt_le_trans. exact H. exact le_lb_pred_ub.
+Qed.
+
+Lemma neq_pred_ub_sb : ∀ sb : nat, sb < lb -> Nat.pred ub ≠ sb.
+Proof using gtlb.
+  intros * H Habs. eapply lt_not_le. 2: eapply le_lb_pred_ub.
+  rewrite Habs. exact H.
+Qed.
+
+Definition smaller_bound : ∀ sb : nat, sb < lb -> greater_than sb.
+Proof using gtlb.
+  intros * H. constructor 1 with ub. apply lt_sb_ub, H.
+Defined.
+
+Lemma smaller_bound_ub : ∀ (sb : nat) (H : sb < lb),
+  @ub sb (smaller_bound H) = @ub lb gtlb.
+Proof using . reflexivity. Qed.
+
+End greater_than.
+
 Section mod2fin.
 
-Context {n : nat}.
+Context {lb : nat} {gtlb : greater_than lb}.
+
+Definition greater_than_0 : greater_than 0.
+Proof using gtlb.
+  destruct (Nat.eq_dec 0 lb) as [Hd | Hd]. { subst. exact gtlb. }
+  apply smaller_bound, neq_0_lt, Hd.
+Defined.
+
+Lemma greater_than_0_ub : @ub 0 greater_than_0 = @ub lb gtlb.
+Proof using .
+  unfold greater_than_0. destruct (Nat.eq_dec 0 lb) as [Hd | Hd].
+  { subst. reflexivity. } apply smaller_bound_ub.
+Qed.
+
+Lemma lt_0_ub : 0 < ub.
+Proof using . rewrite <- greater_than_0_ub. apply lt_lb_ub. Qed.
+
+Lemma neq_ub_0 : ub ≠ 0.
+Proof using gtlb. rewrite <- greater_than_0_ub. apply neq_ub_lb. Qed.
+
+Lemma le_0_pred_ub : 0 <= Nat.pred ub.
+Proof using gtlb. rewrite <- greater_than_0_ub. apply le_lb_pred_ub. Qed.
 
-Lemma mod2fin_lt : ∀ m : nat, m mod (S n) < S n.
-Proof using . intros. apply Nat.mod_upper_bound, Nat.neq_succ_0. Qed.
+Lemma mod2fin_lt : ∀ m : nat, m mod ub < ub.
+Proof using . intros. apply Nat.mod_upper_bound, neq_ub_0. Qed.
 
-Definition mod2fin (m : nat) : fin (S n) := Fin (mod2fin_lt m).
+Definition mod2fin (m : nat) : fin ub := Fin (mod2fin_lt m).
 
 Definition mod2fin_compat : Proper (equiv ==> equiv) mod2fin := _.
 
-Lemma mod2fin_mod : ∀ m : nat, mod2fin (m mod (S n)) = mod2fin m.
+Lemma mod2fin_mod : ∀ m : nat, mod2fin (m mod ub) = mod2fin m.
 Proof using .
-  intros. apply fin2nat_inj. cbn-[Nat.modulo].
-  apply Nat.mod_mod, Nat.neq_succ_0.
+  intros. apply fin2nat_inj. cbn-[Nat.modulo]. apply Nat.mod_mod, neq_ub_0.
 Qed.
 
-Lemma mod2fin2nat : ∀ m : nat, fin2nat (mod2fin m) = m mod (S n).
+Lemma mod2fin2nat : ∀ m : nat, fin2nat (mod2fin m) = m mod ub.
 Proof using . intros. reflexivity. Qed.
 
-Lemma mod2finK : ∀ f : fin (S n), mod2fin f = f.
+Lemma mod2finK : ∀ f : fin ub, mod2fin f = f.
 Proof using . intros. apply fin2nat_inj, Nat.mod_small, fin_lt. Qed.
 
 Lemma mod2fin_locally_inj : ∀ m1 m2 : nat, m1 <= m2
-  -> m2 - m1 < S n -> mod2fin m1 = mod2fin m2 -> m1 = m2.
+  -> m2 - m1 < ub -> mod2fin m1 = mod2fin m2 -> m1 = m2.
 Proof using .
-  intros * Hleq Hsub Heq. eapply mod_locally_inj. apply Nat.neq_succ_0.
+  intros * Hleq Hsub Heq. eapply mod_locally_inj. apply neq_ub_0.
   exact Hleq. exact Hsub. rewrite <-2 mod2fin2nat, Heq. reflexivity.
 Qed.
 
-Lemma mod2fin_bounded_diff_inj : ∀ p m1 m2 : nat, bounded_diff (S n) p m1
-  -> bounded_diff (S n) p m2 -> mod2fin m1 = mod2fin m2 -> m1 = m2.
+Lemma mod2fin_bounded_diff_inj : ∀ p m1 m2 : nat, bounded_diff ub p m1
+  -> bounded_diff ub p m2 -> mod2fin m1 = mod2fin m2 -> m1 = m2.
 Proof using .
   intros p. eapply (locally_bounded_diff _
-  (inj_sym _ _ nat_Setoid (eq_setoid (fin (S n))) mod2fin)).
+  (inj_sym _ _ nat_Setoid (eq_setoid (fin ub)) mod2fin)).
   intros * H1 H2. apply mod2fin_locally_inj. all: assumption.
 Qed.
 
-Definition fin0 : fin (S n) := Fin (Nat.lt_0_succ _).
+Definition fin0 : fin ub := Fin lt_0_ub.
 
 Lemma fin02nat : fin2nat fin0 = 0.
 Proof using . reflexivity. Qed.
 
 Lemma mod2fin0 : mod2fin 0 = fin0.
 Proof using .
-  apply fin2nat_inj. rewrite mod2fin2nat, fin02nat. apply Nat.mod_0_l.
-  exact (Nat.neq_succ_0 _).
+  apply fin2nat_inj. rewrite mod2fin2nat, fin02nat.
+  apply Nat.mod_0_l, neq_ub_0.
 Qed.
 
-Definition addm (f : fin (S n)) (m : nat) : fin (S n) := mod2fin (f + m).
+Definition addm (f : fin ub) (m : nat) : fin ub := mod2fin (f + m).
 
-Definition addn_compat : Proper (equiv ==> equiv ==> equiv) addm := _.
+Definition addm_compat : Proper (equiv ==> equiv ==> equiv) addm := _.
 
-Lemma addm2nat : ∀ (f : fin (S n)) (m : nat),
-  fin2nat (addm f m) = (f + m) mod (S n).
+Lemma addm2nat : ∀ (f : fin ub) (m : nat),
+  fin2nat (addm f m) = (f + m) mod ub.
 Proof using . unfold addm. intros. apply mod2fin2nat. Qed.
 
-Lemma addm_mod : ∀ (f : fin (S n)) (m : nat), addm f (m mod (S n)) = addm f m.
+Lemma addm_mod : ∀ (f : fin ub) (m : nat), addm f (m mod ub) = addm f m.
 Proof using .
   intros. apply fin2nat_inj. rewrite 2 addm2nat.
-  apply Nat.add_mod_idemp_r, Nat.neq_succ_0.
+  apply Nat.add_mod_idemp_r, neq_ub_0.
 Qed.
 
 Lemma addIm : ∀ m : nat,
-  Preliminary.injective equiv equiv (λ f : fin (S n), addm f m).
+  Preliminary.injective equiv equiv (λ f : fin ub, addm f m).
 Proof using .
   intros * f1 f2 H. eapply fin2nat_inj, (Nat.add_cancel_r _ _ m).
-  destruct (le_ge_dec (f1 + m) (f2 + m)) as [Hd|Hd]. 2: symmetry; symmetry in H.
-  all: apply mod2fin_locally_inj. 1,4: exact Hd. 2,4: exact H.
-  rewrite (Nat.add_comm f1). 2: rewrite (Nat.add_comm f2).
-  all: rewrite Nat.sub_add_distr, Nat.add_sub. all: apply <- Nat.add_lt_mono_r.
-  all: rewrite Nat.sub_add. 1,3: apply lt_plus_trans, fin_lt.
-  all: eapply Nat.add_le_mono_r, Hd.
+  eapply (@mod2fin_bounded_diff_inj m). 3: apply H. all: split.
+  1,3: apply le_plus_r. all: rewrite Nat.add_comm. all: apply Nat.add_lt_mono_l,
+  fin_lt.
 Qed.
 
 Lemma addm_locally_inj :
-  ∀ (f : fin (S n)) (m1 m2 : nat), m1 <= m2 -> m2 - m1 < S n
+  ∀ (f : fin ub) (m1 m2 : nat), m1 <= m2 -> m2 - m1 < ub
   -> addm f m1 = addm f m2 -> m1 = m2.
 Proof using .
   unfold addm. intros * Hle Hsu Heq. eapply plus_reg_l, mod2fin_locally_inj.
@@ -120,53 +190,53 @@ Proof using .
   rewrite <- minus_plus_simpl_l_reverse. exact Hsu.
 Qed.
 
-Lemma addm_bounded_diff_inj : ∀ (p : nat) (f : fin (S n)) (m1 m2 : nat),
-  bounded_diff (S n) p m1 -> bounded_diff (S n) p m2
+Lemma addm_bounded_diff_inj : ∀ (p : nat) (f : fin ub) (m1 m2 : nat),
+  bounded_diff ub p m1 -> bounded_diff ub p m2
   -> addm f m1 = addm f m2 -> m1 = m2.
 Proof using .
   intros p f. eapply (locally_bounded_diff _
-  (inj_sym _ _ nat_Setoid (eq_setoid (fin (S n))) (λ x, addm f x))).
+  (inj_sym _ _ nat_Setoid (eq_setoid (fin ub)) (λ x, addm f x))).
   intros *. apply addm_locally_inj.
 Qed.
 
-Lemma addm_comp : ∀ (f : fin (S n)) (m2 m1 : nat),
+Lemma addm_comp : ∀ (f : fin ub) (m2 m1 : nat),
   addm (addm f m1) m2 = addm f (m1 + m2).
 Proof using .
   intros. apply fin2nat_inj. rewrite 3 addm2nat, Nat.add_mod_idemp_l,
-  Nat.add_assoc by apply Nat.neq_succ_0. reflexivity.
+  Nat.add_assoc by apply neq_ub_0. reflexivity.
 Qed.
 
-Lemma addmAC : ∀ (f : fin (S n)) (m1 m2 : nat),
+Lemma addmAC : ∀ (f : fin ub) (m1 m2 : nat),
   addm (addm f m1) m2 = addm (addm f m2) m1.
 Proof using . intros. rewrite 2 addm_comp, Nat.add_comm. reflexivity. Qed.
 
-Lemma addm0 : ∀ f : fin (S n), addm f 0 = f.
+Lemma addm0 : ∀ f : fin ub, addm f 0 = f.
 Proof using .
   intros. apply fin2nat_inj. rewrite addm2nat, Nat.add_0_r,
   Nat.mod_small by apply fin_lt. reflexivity.
 Qed.
 
-Lemma add0m : ∀ f : fin (S n), addm fin0 f = f.
+Lemma add0m : ∀ f : fin ub, addm fin0 f = f.
 Proof using .
   intros. apply fin2nat_inj. rewrite addm2nat, Nat.add_0_l, Nat.mod_small.
   reflexivity. apply fin_lt.
 Qed.
 
-Lemma addm_fin0_divide : ∀ (f : fin (S n)) (m : nat),
-  Nat.divide (S n) (f + m) <-> addm f m = fin0.
+Lemma addm_fin0_divide : ∀ (f : fin ub) (m : nat),
+  Nat.divide ub (f + m) <-> addm f m = fin0.
 Proof using .
-  intros. rewrite <- Nat.mod_divide by apply Nat.neq_succ_0. split; intros H.
+  intros. rewrite <- Nat.mod_divide by apply neq_ub_0. split; intros H.
   - apply fin2nat_inj. rewrite addm2nat, fin02nat. apply H.
   - rewrite <- fin02nat, <- addm2nat. f_equal. apply H.
 Qed.
 
-Lemma addm_addm2nat : ∀ (f1 f2 : fin (S n)) (m : nat),
+Lemma addm_addm2nat : ∀ (f1 f2 : fin ub) (m : nat),
   addm f2 (addm f1 m) = addm (addm f2 f1) m.
 Proof using .
   intros. rewrite addm_comp, addm2nat, addm_mod. reflexivity.
 Qed.
 
-Lemma addmC : ∀ f1 f2 : fin (S n), addm f1 f2 = addm f2 f1.
+Lemma addmC : ∀ f1 f2 : fin ub, addm f1 f2 = addm f2 f1.
 Proof using .
   intros. apply fin2nat_inj. rewrite 2 addm2nat, Nat.add_comm. reflexivity.
 Qed.
@@ -174,101 +244,101 @@ Qed.
 Lemma mod2fin_addm : ∀ 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 Nat.neq_succ_0.
+  Nat.add_mod_idemp_l. reflexivity. apply neq_ub_0.
 Qed.
 
-Definition fin_max : fin (S n) := Fin (Nat.lt_succ_diag_r _).
+Definition fin_max : fin ub := Fin lt_pred_ub.
 
 Lemma addm_fin_max : addm fin_max 1 = fin0.
 Proof using .
-  apply fin2nat_inj. rewrite addm2nat, (Nat.add_1_r (fin2nat _)), Nat.mod_same
-  by apply Nat.neq_succ_0. reflexivity.
+  apply fin2nat_inj. rewrite addm2nat, Nat.add_1_r. cbn.
+  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 Nat.neq_succ_0.
+  Nat.add_mod_idemp_l. reflexivity. apply neq_ub_0.
 Qed.
 
-Definition addf (f1 f2 : fin (S n)) : fin (S n) := addm f1 f2.
+Definition addf (f1 f2 : fin ub) : fin ub := addm f1 f2.
 
 Definition addf_compat : Proper (equiv ==> equiv ==> equiv) addf := _.
 
-Lemma addf2nat : ∀ f1 f2 : fin (S n),
-  fin2nat (addf f1 f2) = (f1 + f2) mod (S n).
+Lemma addf2nat : ∀ f1 f2 : fin ub,
+  fin2nat (addf f1 f2) = (f1 + f2) mod ub.
 Proof using . intros. apply addm2nat. Qed.
 
-Lemma addf_fin0_divide : ∀ f1 f2 : fin (S n),
-  Nat.divide (S n) (f1 + f2) <-> addf f1 f2 = fin0.
+Lemma addf_fin0_divide : ∀ f1 f2 : fin ub,
+  Nat.divide ub (f1 + f2) <-> addf f1 f2 = fin0.
 Proof using . intros. apply addm_fin0_divide. Qed.
 
-Lemma addfC : ∀ f1 f2 : fin (S n), addf f1 f2 = addf f2 f1.
+Lemma addfC : ∀ f1 f2 : fin ub, addf f1 f2 = addf f2 f1.
 Proof using .
   intros. apply fin2nat_inj. rewrite 2 addf2nat, Nat.add_comm. reflexivity.
 Qed.
 
-Lemma add0f : ∀ f : fin (S n), addf fin0 f = f.
+Lemma add0f : ∀ f : fin ub, addf fin0 f = f.
 Proof using . apply add0m. Qed.
 
-Lemma addf0 : ∀ f : fin (S n), addf f fin0 = f.
+Lemma addf0 : ∀ f : fin ub, addf f fin0 = f.
 Proof using . apply addm0. Qed.
 
-Lemma addIf : ∀ f1 : fin (S n),
+Lemma addIf : ∀ f1 : fin ub,
   Preliminary.injective equiv equiv (λ f2, addf f2 f1).
 Proof using . intros f1 f2 f3. apply addIm. Qed.
 
-Lemma addfI : ∀ f1 : fin (S n),
+Lemma addfI : ∀ f1 : fin ub,
   Preliminary.injective equiv equiv (λ f2, addf f1 f2).
 Proof using .
   intros f1 f2 f3 H. eapply addIf. setoid_rewrite addfC. apply H.
 Qed.
 
-Lemma addfA : ∀ f1 f2 f3 : fin (S n),
+Lemma addfA : ∀ f1 f2 f3 : fin ub,
   addf f1 (addf f2 f3) = addf (addf f1 f2) f3.
 Proof using .
   intros. apply fin2nat_inj. rewrite 4 addf2nat, Nat.add_mod_idemp_l,
-  Nat.add_mod_idemp_r, Nat.add_assoc. reflexivity. all: apply Nat.neq_succ_0.
+  Nat.add_mod_idemp_r, Nat.add_assoc. reflexivity. all: apply neq_ub_0.
 Qed.
 
-Lemma addfCA : ∀ f1 f2 f3 : fin (S n),
+Lemma addfCA : ∀ f1 f2 f3 : fin ub,
   addf f1 (addf f2 f3) = addf f2 (addf f1 f3).
 Proof using .
   intros. rewrite (addfC f2 f3), addfA, (addfC (addf _ _) _). reflexivity.
 Qed.
 
-Lemma addfAC : ∀ f1 f2 f3 : fin (S n),
+Lemma addfAC : ∀ f1 f2 f3 : fin ub,
   addf (addf f1 f2) f3 = addf (addf f1 f3) f2.
 Proof using . intros. apply addmAC. Qed.
 
-Lemma addfACA : ∀ f1 f2 f3 f4 : fin (S n),
+Lemma addfACA : ∀ f1 f2 f3 f4 : fin ub,
   addf (addf f1 f2) (addf f3 f4) = addf (addf f1 f3) (addf f2 f4).
 Proof using . intros. rewrite 2 addfA, (addfAC f1 f3 f2). reflexivity. Qed.
 
-Lemma addf_addm : ∀ f1 f2 : fin (S n), addf f1 f2 = addm f1 f2.
+Lemma addf_addm : ∀ f1 f2 : fin ub, addf f1 f2 = addm f1 f2.
 Proof using . reflexivity. Qed.
 
-Lemma addm_addf : ∀ (f : fin (S n)) (m : nat), addm f m = addf f (mod2fin m).
+Lemma addm_addf : ∀ (f : fin ub) (m : nat), addm f m = addf f (mod2fin m).
 Proof using .
   intros. rewrite addf_addm, mod2fin2nat, addm_mod. reflexivity.
 Qed.
 
-Lemma rev_fin_subproof : ∀ f : fin (S n), n - f < S n.
+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 Nat.lt_succ_diag_r.
+  intros. eapply Nat.le_lt_trans. apply Nat.le_sub_l. apply lt_pred_ub.
 Qed.
 
-Definition rev_fin (f : fin (S n)) : fin (S n) := Fin (rev_fin_subproof f).
+Definition rev_fin (f : fin ub) : fin ub := Fin (rev_fin_subproof f).
 
 Definition rev_fin_compat : Proper (equiv ==> equiv) rev_fin := _.
 
-Lemma rev_fin2nat : ∀ f : fin (S n), fin2nat (rev_fin f) = n - f.
+Lemma rev_fin2nat : ∀ f : fin ub, fin2nat (rev_fin f) = Nat.pred ub - f.
 Proof using . reflexivity. Qed.
 
-Lemma rev_finK : ∀ f : fin (S n), rev_fin (rev_fin f) = f.
+Lemma rev_finK : ∀ f : fin ub, rev_fin (rev_fin f) = f.
 Proof using .
   intros. apply fin2nat_inj. rewrite 2 rev_fin2nat, sub_sub, minus_plus.
-  reflexivity. apply lt_n_Sm_le, fin_lt.
+  reflexivity. apply fin_le.
 Qed.
 
 Lemma rev_fin_inj : Preliminary.injective equiv equiv rev_fin.
@@ -276,81 +346,81 @@ Proof using .
   intros f1 f2 H. setoid_rewrite <- rev_finK. rewrite H. reflexivity.
 Qed.
 
-Definition oppf (f : fin (S n)) : fin (S n) := addm (rev_fin f) 1.
+Definition oppf (f : fin ub) : fin ub := addm (rev_fin f) 1.
 
 Definition oppf_compat : Proper (equiv ==> equiv) oppf := _.
 
-Lemma oppf2nat : ∀ f : fin (S n), fin2nat (oppf f) = (S n - f) mod (S n).
+Lemma oppf2nat : ∀ f : fin ub, fin2nat (oppf f) = (ub - f) mod ub.
 Proof using .
-  intros. unfold oppf. rewrite addm2nat. f_equal. rewrite rev_fin2nat,
-  <- Nat.add_sub_swap, Nat.add_1_r. reflexivity. apply lt_n_Sm_le, fin_lt.
+  intros. unfold oppf. rewrite addm2nat. f_equal. erewrite rev_fin2nat,
+  <- Nat.add_sub_swap, Nat.add_1_r, S_pred_ub. reflexivity. apply fin_le.
 Qed.
 
-Definition oppm (m : nat) : fin (S n) := oppf (mod2fin m).
+Definition oppm (m : nat) : fin ub := oppf (mod2fin m).
 
 Definition oppm_compat : Proper (equiv ==> equiv) oppm := _.
 
 Lemma oppm2nat : ∀ m : nat,
-  fin2nat (oppm m) = (S n - (m mod (S n))) mod (S n).
+  fin2nat (oppm m) = (ub - (m mod ub)) mod ub.
 Proof using .
   intros. unfold oppm. rewrite oppf2nat, mod2fin2nat. reflexivity.
 Qed.
 
-Lemma oppm_mod : ∀ m : nat, oppm (m mod (S n)) = oppm m.
+Lemma oppm_mod : ∀ m : nat, oppm (m mod ub) = oppm m.
 Proof using .
   intros. apply fin2nat_inj. rewrite 2 oppm2nat, Nat.mod_mod.
-  reflexivity. apply Nat.neq_succ_0.
+  reflexivity. apply neq_ub_0.
 Qed.
 
 Lemma oppm_oppf : ∀ m : nat, oppm m = oppf (mod2fin m).
 Proof using . reflexivity. Qed.
 
-Lemma oppf_oppm : ∀ f : fin (S n), oppf f = oppm f.
+Lemma oppf_oppm : ∀ f : fin ub, oppf f = oppm f.
 Proof using . intros. unfold oppm. rewrite mod2finK. reflexivity. Qed.
 
-Lemma oppm_divide : ∀ m : nat, Nat.divide (S n) (m + (oppm m)).
+Lemma oppm_divide : ∀ m : nat, Nat.divide ub (m + (oppm m)).
 Proof using .
   intros. rewrite <- Nat.mod_divide, oppm2nat, Nat.add_mod_idemp_r,
   Nat.add_comm, <- Nat.add_mod_idemp_r, Nat.sub_add. apply Nat.mod_same.
-  2: apply Nat.lt_le_incl, mod2fin_lt. all: apply Nat.neq_succ_0.
+  2: apply Nat.lt_le_incl, mod2fin_lt. all: apply neq_ub_0.
 Qed.
 
-Lemma oppf_divide : ∀ f : fin (S n), Nat.divide (S n) (f + (oppf f)).
+Lemma oppf_divide : ∀ f : fin ub, Nat.divide ub (f + (oppf f)).
 Proof using . intros. rewrite oppf_oppm. apply oppm_divide. Qed.
 
-Lemma addfKoppf : ∀ f : fin (S n), addf (oppf f) f = fin0.
+Lemma addfKoppf : ∀ f : fin ub, addf (oppf f) f = fin0.
 Proof using .
   intros. apply fin2nat_inj. rewrite addf2nat, Nat.add_comm, fin02nat.
-  apply Nat.mod_divide. apply Nat.neq_succ_0. apply oppf_divide. 
+  apply Nat.mod_divide. apply neq_ub_0. apply oppf_divide. 
 Qed.
 
-Lemma oppfKaddf : ∀ f : fin (S n), addf f (oppf f) = fin0.
+Lemma oppfKaddf : ∀ f : fin ub, addf f (oppf f) = fin0.
 Proof using . intros. rewrite addfC. apply addfKoppf. Qed.
 
-Lemma addfOoppf : ∀ f1 f2 : fin (S n), addf (oppf f1) (addf f1 f2) = f2.
+Lemma addfOoppf : ∀ f1 f2 : fin ub, addf (oppf f1) (addf f1 f2) = f2.
 Proof using . intros. rewrite addfA, addfKoppf, add0f. reflexivity. Qed.
 
-Lemma oppfOaddf : ∀ f1 f2 : fin (S n), addf (addf f2 f1) (oppf f1) = f2.
+Lemma oppfOaddf : ∀ f1 f2 : fin ub, addf (addf f2 f1) (oppf f1) = f2.
 Proof using . intros. rewrite addfC, (addfC f2 f1). apply addfOoppf. Qed.
 
-Lemma addfOVoppf : ∀ f1 f2 : fin (S n), addf f1 (addf (oppf f1) f2) = f2.
+Lemma addfOVoppf : ∀ f1 f2 : fin ub, addf f1 (addf (oppf f1) f2) = f2.
 Proof using . intros. rewrite (addfC _ f2), addfCA, oppfKaddf. apply addf0. Qed.
 
-Lemma oppfOVaddf : ∀ f1 f2 : fin (S n), addf (addf f2 (oppf f1)) f1 = f2.
+Lemma oppfOVaddf : ∀ f1 f2 : fin ub, addf (addf f2 (oppf f1)) f1 = f2.
 Proof using . intros. rewrite addfC, (addfC f2 _). apply addfOVoppf. Qed.
 
 Lemma oppfI : Preliminary.injective equiv equiv oppf.
 Proof using . intros f1 f2 H. eapply rev_fin_inj, addIm, H. Qed.
 
 Lemma oppm_locally_inj : ∀ m1 m2 : nat, m1 <= m2
-  -> m2 - m1 < S n -> oppm m1 = oppm m2 -> m1 = m2.
+  -> m2 - m1 < ub -> oppm m1 = oppm m2 -> m1 = m2.
 Proof using .
   intros * Hleq Hsub Heq. eapply mod2fin_locally_inj, oppfI, Heq.
   apply Hleq. apply Hsub.
 Qed.
 
 Lemma oppm_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
-  bounded_diff (S n) p m1 -> bounded_diff (S n) p m2
+  bounded_diff ub p m1 -> bounded_diff ub p m2
   -> oppm m1 = oppm m2 -> m1 = m2.
 Proof using .
   rewrite <- locally_bounded_diff. apply oppm_locally_inj.
@@ -360,65 +430,65 @@ Qed.
 Lemma oppf0 : oppf fin0 = fin0.
 Proof using .
   apply fin2nat_inj. rewrite oppf2nat, fin02nat, Nat.sub_0_r.
-  apply Nat.mod_same. apply Nat.neq_succ_0.
+  apply Nat.mod_same. apply neq_ub_0.
 Qed.
 
 Lemma oppm0 : oppm 0 = fin0.
 Proof using . rewrite oppm_oppf, mod2fin0. apply oppf0. Qed.
 
-Definition subm (f : fin (S n)) (m : nat) : fin (S n) := addm f (oppm m).
+Definition subm (f : fin ub) (m : nat) : fin ub := addm f (oppm m).
 
-Definition subf (f1 f2 : fin (S n)) : fin (S n) := addf f1 (oppf f2).
+Definition subf (f1 f2 : fin ub) : fin ub := addf f1 (oppf f2).
 
 Definition subm_compat : Proper (equiv ==> equiv ==> equiv) subm := _.
 
 Definition subf_compat : Proper (equiv ==> equiv ==> equiv) subf := _.
 
-Lemma subf_subm : ∀ f1 f2 : fin (S n), subf f1 f2 = subm f1 f2.
+Lemma subf_subm : ∀ f1 f2 : fin ub, subf f1 f2 = subm f1 f2.
 Proof using . intros. unfold subf, subm. rewrite oppf_oppm. reflexivity. Qed.
 
-Lemma subm_subf : ∀ (f : fin (S n)) (m : nat), subm f m = subf f (mod2fin m).
+Lemma subm_subf : ∀ (f : fin ub) (m : nat), subm f m = subf f (mod2fin m).
 Proof using .
   intros. unfold subf, subm. rewrite oppm_oppf, addf_addm. reflexivity.
 Qed.
 
-Lemma subm2nat : ∀ (f : fin (S n)) (m : nat),
-  fin2nat (subm f m) = (f + (S n - (m mod (S n)))) mod (S n).
+Lemma subm2nat : ∀ (f : fin ub) (m : nat),
+  fin2nat (subm f m) = (f + (ub - (m mod ub))) mod ub.
 Proof using .
   intros. unfold subm. rewrite addm2nat, oppm2nat, Nat.add_mod_idemp_r.
-  reflexivity. apply Nat.neq_succ_0.
+  reflexivity. apply neq_ub_0.
 Qed.
 
-Lemma subf2nat : ∀ f1 f2 : fin (S n),
-  fin2nat (subf f1 f2) = (f1 + (S n - f2)) mod (S n).
+Lemma subf2nat : ∀ f1 f2 : fin ub,
+  fin2nat (subf f1 f2) = (f1 + (ub - f2)) mod ub.
 Proof using .
   intros. rewrite subf_subm, subm2nat, (Nat.mod_small f2). reflexivity.
   apply fin_lt.
 Qed.
 
-Lemma subfE : ∀ f1 f2 : fin (S n), subf f1 f2 = addf f1 (oppf f2).
+Lemma subfE : ∀ f1 f2 : fin ub, subf f1 f2 = addf f1 (oppf f2).
 Proof using . reflexivity. Qed.
 
-Lemma submE : ∀ (f : fin (S n)) (m : nat), subm f m = addm f (oppm m).
+Lemma submE : ∀ (f : fin ub) (m : nat), subm f m = addm f (oppm m).
 Proof using . reflexivity. Qed.
 
-Lemma oppf_rev_fin : ∀ f : fin (S n), oppf f = addm (rev_fin f) 1.
+Lemma oppf_rev_fin : ∀ f : fin ub, oppf f = addm (rev_fin f) 1.
 Proof using . reflexivity. Qed.
 
-Lemma rev_fin_oppf : ∀ f : fin (S n), rev_fin f = subm (oppf f) 1.
+Lemma rev_fin_oppf : ∀ f : fin ub, rev_fin f = subm (oppf f) 1.
 Proof using .
   intros. rewrite submE, oppf_rev_fin, oppm_oppf, 2 addm_addf, mod2finK,
   oppfOaddf. reflexivity.
 Qed.
 
-Lemma subm_mod : ∀ (f : fin (S n)) (m : nat), subm f (m mod (S n)) = subm f m.
+Lemma subm_mod : ∀ (f : fin ub) (m : nat), subm f (m mod ub) = subm f m.
 Proof using . intros. rewrite 2 subm_subf, mod2fin_mod. reflexivity. Qed.
 
-Lemma subIf : ∀ f1 : fin (S n),
+Lemma subIf : ∀ f1 : fin ub,
   Preliminary.injective equiv equiv (λ f2, subf f2 f1).
 Proof using . intros f1 f2 f3 H. eapply addIf, H. Qed.
 
-Lemma subfI : ∀ f1 : fin (S n),
+Lemma subfI : ∀ f1 : fin ub,
   Preliminary.injective equiv equiv (λ f2, subf f1 f2).
 Proof using . intros f1 f2 f3 H. eapply oppfI, addfI, H. Qed.
 
@@ -426,76 +496,76 @@ Lemma subIm : ∀ m : nat,
   Preliminary.injective equiv equiv (λ f, subm f m).
 Proof using . intros m f1 f2. rewrite 2 subm_subf. apply subIf. Qed.
 
-Lemma subm_locally_inj : ∀ (f : fin (S n)) (m1 m2 : nat),
-  m1 <= m2 -> m2 - m1 < S n -> subm f m1 = subm f m2 -> m1 = m2.
+Lemma subm_locally_inj : ∀ (f : fin ub) (m1 m2 : nat),
+  m1 <= m2 -> m2 - m1 < ub -> subm f m1 = subm f m2 -> m1 = m2.
 Proof using .
   intros * Hle Hsu. rewrite 2 subm_subf. intros Heq. eapply mod2fin_locally_inj,
   subfI. all: eassumption.
 Qed.
 
-Lemma subm_bounded_diff_inj : ∀ (p : nat) (f : fin (S n)) (m1 m2 : nat),
-  bounded_diff (S n) p m1 -> bounded_diff (S n) p m2
+Lemma subm_bounded_diff_inj : ∀ (p : nat) (f : fin ub) (m1 m2 : nat),
+  bounded_diff ub p m1 -> bounded_diff ub p m2
   -> subm f m1 = subm f m2 -> m1 = m2.
 Proof using .
   intros p f. eapply (locally_bounded_diff _
-  (inj_sym _ _ nat_Setoid (eq_setoid (fin (S n))) (λ x, subm f x))).
+  (inj_sym _ _ nat_Setoid (eq_setoid (fin ub)) (λ x, subm f x))).
   intros *. apply subm_locally_inj.
 Qed.
 
-Lemma sub0f : ∀ f : fin (S n), subf fin0 f = oppf f.
+Lemma sub0f : ∀ f : fin ub, subf fin0 f = oppf f.
 Proof using . intros. unfold subf. apply add0f. Qed.
 
 Lemma sub0m : ∀ m : nat, subm fin0 m = oppm m.
 Proof using . intros. unfold subm. apply add0m. Qed.
 
-Lemma subf0 : ∀ f : fin (S n), subf f fin0 = f.
+Lemma subf0 : ∀ f : fin ub, subf f fin0 = f.
 Proof using . intros. unfold subf. rewrite oppf0. apply addf0. Qed.
 
-Lemma subm0 : ∀ f : fin (S n), subm f 0 = f.
+Lemma subm0 : ∀ f : fin ub, subm f 0 = f.
 Proof using . intros. rewrite subm_subf, mod2fin0. apply subf0. Qed.
 
-Lemma subfAC : ∀ f1 f2 f3 : fin (S n),
+Lemma subfAC : ∀ f1 f2 f3 : fin ub,
   subf (subf f1 f2) f3 = subf (subf f1 f3) f2.
 Proof using . intros. unfold subf. rewrite addfAC. reflexivity. Qed.
 
-Lemma submAC : ∀ (f : fin (S n)) (m1 m2 : nat),
+Lemma submAC : ∀ (f : fin ub) (m1 m2 : nat),
   subm (subm f m1) m2 = subm (subm f m2) m1.
 Proof using . intros f m1 m2. unfold subm. rewrite addmAC. reflexivity. Qed.
 
-Lemma subff : ∀ f : fin (S n), subf f f = fin0.
+Lemma subff : ∀ f : fin ub, subf f f = fin0.
 Proof using . intros. unfold subf. apply oppfKaddf. Qed.
 
-Lemma submm : ∀ f : fin (S n), subm f f = fin0.
+Lemma submm : ∀ f : fin ub, subm f f = fin0.
 Proof using . intros. rewrite subm_subf, mod2finK. apply subff. Qed.
 
 Lemma submKmod2fin : ∀ m : nat, subm (mod2fin m) m = fin0.
 Proof using . intros. rewrite subm_subf. apply subff. Qed.
 
-Lemma fin2natKsubm : ∀ f : fin (S n), subm f f = fin0.
+Lemma fin2natKsubm : ∀ f : fin ub, subm f f = fin0.
 Proof using . intros. rewrite subm_subf, mod2finK. apply subff. Qed.
 
-Lemma addfKV : ∀ f1 f2 : fin (S n), subf (addf f1 f2) f1 = f2.
+Lemma addfKV : ∀ f1 f2 : fin ub, subf (addf f1 f2) f1 = f2.
 Proof using . intros. rewrite addfC, subfE. apply oppfOaddf. Qed.
 
-Lemma addfVKV : ∀ f1 f2 : fin (S n), subf (addf f2 f1) f1 = f2.
+Lemma addfVKV : ∀ f1 f2 : fin ub, subf (addf f2 f1) f1 = f2.
 Proof using . intros. rewrite addfC. apply addfKV. Qed.
 
-Lemma subfVK : ∀ f1 f2 : fin (S n), addf f1 (subf f2 f1) = f2.
+Lemma subfVK : ∀ f1 f2 : fin ub, addf f1 (subf f2 f1) = f2.
 Proof using . intros. eapply subIf. rewrite addfKV. reflexivity. Qed.
 
-Lemma subfVKV : ∀ f1 f2 : fin (S n), addf (subf f2 f1) f1 = f2.
+Lemma subfVKV : ∀ f1 f2 : fin ub, addf (subf f2 f1) f1 = f2.
 Proof using . intros. rewrite addfC. apply subfVK. Qed.
 
-Lemma addmVKV : ∀ (m : nat) (f : fin (S n)), subm (addm f m) m = f.
+Lemma addmVKV : ∀ (m : nat) (f : fin ub), subm (addm f m) m = f.
 Proof using . intros. rewrite subm_subf, addm_addf. apply addfVKV. Qed.
 
-Lemma submVKV : ∀ (m : nat) (f : fin (S n)), addm (subm f m) m = f.
+Lemma submVKV : ∀ (m : nat) (f : fin ub), addm (subm f m) m = f.
 Proof using . intros. rewrite subm_subf, addm_addf. apply subfVKV. Qed.
 
 Lemma subm_fin_max : subm fin0 1 = fin_max.
 Proof using . rewrite <- addm_fin_max, subm_subf, addm_addf. apply addfVKV. Qed.
 
-Lemma oppf_addf : ∀ f1 f2 : fin (S n), oppf (addf f1 f2) = subf (oppf f1) f2.
+Lemma oppf_addf : ∀ f1 f2 : fin ub, oppf (addf f1 f2) = subf (oppf f1) f2.
 Proof using .
   intros. apply fin2nat_inj. rewrite subf2nat, 2 oppf2nat, addf2nat,
   Nat.add_mod_idemp_l, Nat.add_sub_assoc, <- Nat.add_sub_swap,
@@ -503,89 +573,89 @@ Proof using .
   <- Nat.add_sub_swap, (Nat.mod_eq (_ + _)), sub_sub,
   (Nat.add_sub_swap _ (_ * _)), Nat.mul_comm, Nat.mod_add. reflexivity.
   3: apply Nat.mul_div_le. 2: apply Nat.add_le_mono.
-  1,4,5,7,10: apply Nat.neq_succ_0. all: apply Nat.lt_le_incl.
+  1,4,5,7,10: apply neq_ub_0. all: apply Nat.lt_le_incl.
   3: apply mod2fin_lt. all: apply fin_lt.
 Qed.
 
-Lemma oppf_subf : ∀ f1 f2 : fin (S n), oppf (subf f1 f2) = subf f2 f1.
+Lemma oppf_subf : ∀ f1 f2 : fin ub, oppf (subf f1 f2) = subf f2 f1.
 Proof using .
   intros. eapply subIf. rewrite <- oppf_addf, subfVKV, subfAC, subff, sub0f. 
   reflexivity.
 Qed.
 
-Lemma oppf_subm : ∀ (f : fin (S n)) (m : nat),
+Lemma oppf_subm : ∀ (f : fin ub) (m : nat),
   oppf (subm f m) = subf (mod2fin m) f.
 Proof using . intros. rewrite subm_subf. apply oppf_subf. Qed.
 
-Lemma oppfK : ∀ f : fin (S n), oppf (oppf f) = f.
+Lemma oppfK : ∀ f : fin ub, oppf (oppf f) = f.
 Proof using . intros. rewrite <- (sub0f f), oppf_subf. apply subf0. Qed.
 
 Lemma oppmK : ∀ m : nat, oppm (oppm m) = mod2fin m.
 Proof using . intros. rewrite 2 oppm_oppf, mod2finK. apply oppfK. Qed.
 
-Lemma oppf_add : ∀ f : fin (S n), f ≠ fin0 -> f + oppf f = S n.
+Lemma oppf_add : ∀ f : fin ub, f ≠ fin0 -> f + oppf f = ub.
 Proof using .
   intros f H. rewrite oppf2nat, Nat.mod_small. symmetry. apply le_plus_minus.
   2: apply Nat.sub_lt. 1,2: apply Nat.lt_le_incl, fin_lt. apply neq_0_lt.
   intros Habs. elim H. apply fin2nat_inj. rewrite fin02nat, Habs. reflexivity.
 Qed.
 
-Lemma addfE : ∀ f1 f2 : fin (S n), addf f1 f2 = subf f1 (oppf f2).
+Lemma addfE : ∀ f1 f2 : fin ub, addf f1 f2 = subf f1 (oppf f2).
 Proof using . intros. rewrite subfE, oppfK. reflexivity. Qed.
 
-Lemma addmE : ∀ (f : fin (S n)) (m : nat), addm f m = subm f (oppm m).
+Lemma addmE : ∀ (f : fin ub) (m : nat), addm f m = subm f (oppm m).
 Proof using .
   intros. rewrite submE, oppmK, mod2fin2nat. symmetry. apply addm_mod.
 Qed.
 
-Lemma subfA : ∀ f1 f2 f3 : fin (S n),
+Lemma subfA : ∀ f1 f2 f3 : fin ub,
   subf f1 (subf f2 f3) = subf (addf f1 f3) f2.
 Proof using .
   intros. rewrite 3subfE, oppf_addf, subfE, oppfK, addfA. apply addfAC.
 Qed.
 
-Lemma addf_subf : ∀ f1 f2 f3 : fin (S n),
+Lemma addf_subf : ∀ f1 f2 f3 : fin ub,
   addf (subf f1 f2) f3 = subf (addf f1 f3) f2.
 Proof using . intros. rewrite addfE, subfAC, <- addfE. reflexivity. Qed.
 
-Lemma addm_subm : ∀ (f : fin (S n)) (m1 m2 : nat),
+Lemma addm_subm : ∀ (f : fin ub) (m1 m2 : nat),
   addm (subm f m2) m1 = subm (addm f m1) m2.
 Proof using . intros. rewrite 2 addm_addf, 2 subm_subf. apply addf_subf. Qed.
 
-Lemma subf_addf : ∀ f1 f2 f3 : fin (S n),
+Lemma subf_addf : ∀ f1 f2 f3 : fin ub,
   subf f1 (addf f2 f3) = subf (subf f1 f2) f3.
 Proof using .
   intros. rewrite 3 subfE, <- addfA, oppf_addf, subfE. reflexivity.
 Qed.
 
-Lemma subf_addf_addf : ∀ f1 f2 f3 : fin (S n),
+Lemma subf_addf_addf : ∀ f1 f2 f3 : fin ub,
   subf (addf f1 f3) (addf f2 f3) = subf f1 f2.
 Proof using . intros. rewrite <- subfA, addfVKV. reflexivity. Qed.
 
-Lemma subf_addm_addm : ∀ (f1 f2 : fin (S n)) (m : nat),
+Lemma subf_addm_addm : ∀ (f1 f2 : fin ub) (m : nat),
   subf (addm f1 m) (addm f2 m) = subf f1 f2.
 Proof using . intros. rewrite 2 addm_addf. apply subf_addf_addf. Qed.
 
-Lemma subm_comp : ∀ (f : fin (S n)) (m2 m1 : nat),
+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.
   reflexivity.
 Qed.
 
-Lemma subfCAC : ∀ f1 f2 f3 f4 : fin (S n),
+Lemma subfCAC : ∀ f1 f2 f3 f4 : fin ub,
   subf (subf f1 f2) (subf f3 f4) = subf (subf f1 f3) (subf f2 f4).
 Proof using .
   intros. rewrite <- subf_addf, addfC, addf_subf, addfC,
   <- addf_subf, addfC, subf_addf. reflexivity.
 Qed.
 
-Definition asbf (f : fin (S n)) : bijection (fin (S n)) :=
-  cancel_bijection (λ f2 : fin (S n), subf f2 f) _ (@addIf f)
+Definition asbf (f : fin ub) : bijection (fin ub) :=
+  cancel_bijection (λ f2 : fin ub, subf f2 f) _ (@addIf f)
                    (addfVKV f) (subfVKV f).
 
-Definition asbm (m : nat) : bijection (fin (S n)) :=
-  cancel_bijection (λ f : fin (S n), subm f m) _ (@addIm m)
+Definition asbm (m : nat) : bijection (fin ub) :=
+  cancel_bijection (λ f : fin ub, subm f m) _ (@addIm m)
                    (addmVKV m) (submVKV m).
 
 Lemma asbmE : ∀ m : nat, asbm m == asbf (mod2fin m).
@@ -594,32 +664,32 @@ Proof using . intros m f. apply addm_addf. Qed.
 Lemma asbmVE : ∀ m : nat, asbm m⁻¹ == asbf (mod2fin m)⁻¹.
 Proof using . intros m f. apply subm_subf. Qed.
 
-Lemma asbfE : ∀ f : fin (S n), asbf f == asbm f.
+Lemma asbfE : ∀ f : fin ub, asbf f == asbm f.
 Proof using . intros f1 f2. apply addf_addm. Qed.
 
-Lemma asbfVE : ∀ f : fin (S n), asbf f⁻¹ == asbm f⁻¹.
+Lemma asbfVE : ∀ f : fin ub, asbf f⁻¹ == asbm f⁻¹.
 Proof using . intros f1 f2. apply subf_subm. Qed.
 
-Lemma asbm2nat : ∀ (m : nat) (f : fin (S n)),
-  fin2nat (asbm m f) = (f + m) mod (S n).
+Lemma asbm2nat : ∀ (m : nat) (f : fin ub),
+  fin2nat (asbm m f) = (f + m) mod ub.
 Proof using . intros. apply addm2nat. Qed.
 
-Lemma asbf2nat : ∀ (f1 f2 : fin (S n)),
-  fin2nat (asbf f1 f2) = (f2 + f1) mod (S n).
+Lemma asbf2nat : ∀ (f1 f2 : fin ub),
+  fin2nat (asbf f1 f2) = (f2 + f1) mod ub.
 Proof using . intros. apply addf2nat. Qed.
 
-Lemma asbmV2nat : ∀ (m : nat) (f : fin (S n)),
-  fin2nat ((asbm m)⁻¹ f) = (f + (S n - (m mod (S n)))) mod (S n).
+Lemma asbmV2nat : ∀ (m : nat) (f : fin ub),
+  fin2nat ((asbm m)⁻¹ f) = (f + (ub - (m mod ub))) mod ub.
 Proof using . intros. apply subm2nat. Qed.
 
-Lemma asbfV2nat : ∀ (f1 f2 : fin (S n)),
-  fin2nat ((asbf f1)⁻¹ f2) = (f2 + (S n - f1)) mod (S n).
+Lemma asbfV2nat : ∀ (f1 f2 : fin ub),
+  fin2nat ((asbf f1)⁻¹ f2) = (f2 + (ub - f1)) mod ub.
 Proof using . intros. apply subf2nat. Qed.
 
-Lemma asbm_mod : ∀ m : nat, asbm (m mod (S n)) == asbm m.
+Lemma asbm_mod : ∀ m : nat, asbm (m mod ub) == asbm m.
 Proof using . intros m f. apply addm_mod. Qed.
 
-Lemma asbmV_mod : ∀ m : nat, (asbm (m mod (S n)))⁻¹ == (asbm m)⁻¹.
+Lemma asbmV_mod : ∀ m : nat, (asbm (m mod ub))⁻¹ == (asbm m)⁻¹.
 Proof using . intros m f. apply subm_mod. Qed.
 
 Lemma asbmI : ∀ m : nat, Preliminary.injective equiv equiv (asbm m).
@@ -628,10 +698,10 @@ Proof using . intros. apply addIm. Qed.
 Lemma asbmVI : ∀ m : nat, Preliminary.injective equiv equiv ((asbm m)⁻¹).
 Proof using . intros. apply subIm. Qed.
 
-Lemma asbfI : ∀ f : fin (S n), Preliminary.injective equiv equiv (asbf f).
+Lemma asbfI : ∀ f : fin ub, Preliminary.injective equiv equiv (asbf f).
 Proof using . intros. apply addIf. Qed.
 
-Lemma asbfVI : ∀ f : fin (S n), Preliminary.injective equiv equiv ((asbm f)⁻¹).
+Lemma asbfVI : ∀ f : fin ub, Preliminary.injective equiv equiv ((asbm f)⁻¹).
 Proof using . intros. apply subIf. Qed.
 
 Lemma asbm0 : asbm 0 == @id _ _.
@@ -646,19 +716,19 @@ Proof using . intros f. apply addf0. Qed.
 Lemma asbfV0 : (asbf fin0)⁻¹ == (@id _ _)⁻¹.
 Proof using . intros f. apply subf0. Qed.
 
-Lemma asb0f : ∀ f : fin (S n), asbf f fin0 = f.
+Lemma asb0f : ∀ f : fin ub, asbf f fin0 = f.
 Proof using . intros. apply add0f. Qed.
 
-Lemma asb0m : ∀ f : fin (S n), asbm f fin0 = f.
+Lemma asb0m : ∀ f : fin ub, asbm f fin0 = f.
 Proof using . intros. apply add0f. Qed.
 
-Lemma asb0fV : ∀ f : fin (S n), (asbf f)⁻¹ fin0 = oppf f.
+Lemma asb0fV : ∀ f : fin ub, (asbf f)⁻¹ fin0 = oppf f.
 Proof using . intros. apply sub0f. Qed.
 
-Lemma asbffV : ∀ f : fin (S n), (asbf f)⁻¹ f = fin0.
+Lemma asbffV : ∀ f : fin ub, (asbf f)⁻¹ f = fin0.
 Proof using . intros. apply subff. Qed.
 
-Lemma asbmmV : ∀ f : fin (S n), (asbm f)⁻¹ f = fin0.
+Lemma asbmmV : ∀ f : fin ub, (asbm f)⁻¹ f = fin0.
 Proof using . intros. apply submm. Qed.
 
 Lemma asbm_fin_max : asbm 1 fin_max = fin0.
@@ -667,10 +737,10 @@ Proof using . apply addm_fin_max. Qed.
 Lemma asbmV_fin_max : (asbm 1)⁻¹ fin0 = fin_max.
 Proof using . apply subm_fin_max. Qed.
 
-Lemma asbfC : ∀ f1 f2 : fin (S n), asbf f1 f2 = asbf f2 f1.
+Lemma asbfC : ∀ f1 f2 : fin ub, asbf f1 f2 = asbf f2 f1.
 Proof using . intros. apply addfC. Qed.
 
-Lemma asbmC : ∀ f1 f2 : fin (S n), asbm f1 f2 = asbm f2 f1.
+Lemma asbmC : ∀ f1 f2 : fin ub, asbm f1 f2 = asbm f2 f1.
 Proof using . intros. apply addfC. Qed.
 
 Lemma asbm_comp : ∀ (m2 m1 : nat), asbm m2 ∘ (asbm m1) == asbm (m1 + m2).
@@ -687,24 +757,24 @@ Lemma asbmVAC : ∀ (m1 m2 : nat),
   (asbm m2)⁻¹ ∘ (asbm m1)⁻¹ == (asbm m1)⁻¹ ∘ (asbm m2)⁻¹.
 Proof using . intros * f. cbn-[subm]. apply submAC. Qed.
 
-Lemma asbm_fin0_divide : ∀ (f : fin (S n)) (m : nat),
-  Nat.divide (S n) (f + m) ↔ asbm m f = fin0.
+Lemma asbm_fin0_divide : ∀ (f : fin ub) (m : nat),
+  Nat.divide ub (f + m) ↔ asbm m f = fin0.
 Proof using . apply addm_fin0_divide. Qed.
 
 Lemma asbm_locally_inj : ∀ m1 m2 : nat,
-  m1 ≤ m2 → m2 - m1 < S n → asbm m1 == asbm m2 → m1 = m2.
+  m1 ≤ m2 → m2 - m1 < ub → asbm m1 == asbm m2 → m1 = m2.
 Proof using .
   intros * ?? H. apply addm_locally_inj with fin0. 3: apply H. all: assumption.
 Qed.
 
 Lemma asbmV_locally_inj : ∀ m1 m2 : nat,
-  m1 ≤ m2 → m2 - m1 < S n → (asbm m1)⁻¹ == (asbm m2)⁻¹ → m1 = m2.
+  m1 ≤ m2 → m2 - m1 < ub → (asbm m1)⁻¹ == (asbm m2)⁻¹ → m1 = m2.
 Proof using .
   intros * ?? H. apply subm_locally_inj with fin0. 3: apply H. all: assumption.
 Qed.
 
 Lemma asbm_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
-  bounded_diff (S n) p m1 → bounded_diff (S n) p m2
+  bounded_diff ub p m1 → bounded_diff ub p m2
   → asbm m1 == asbm m2 → m1 = m2.
 Proof using .
   intros * ?? H. apply addm_bounded_diff_inj with (p:=p) (f:=fin0).
@@ -712,7 +782,7 @@ Proof using .
 Qed.
 
 Lemma asbmV_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
-  bounded_diff (S n) p m1 → bounded_diff (S n) p m2
+  bounded_diff ub p m1 → bounded_diff ub p m2
   → (asbm m1)⁻¹ == (asbm m2)⁻¹ → m1 = m2.
 Proof using .
   intros * ?? H. apply subm_bounded_diff_inj with (p:=p) (f:=fin0).
@@ -723,138 +793,138 @@ Lemma asbmCV : ∀ m1 m2 : nat,
   asbm m1 ∘ (asbm m2)⁻¹ == (asbm m2)⁻¹ ∘ (asbm m1).
 Proof using . intros * f. cbn-[addm subm]. apply addm_subm. Qed.
 
-Lemma asbfCV : ∀ f1 f2 : fin (S n),
+Lemma asbfCV : ∀ f1 f2 : fin ub,
   asbf f1 ∘ (asbf f2)⁻¹ == (asbf f2)⁻¹ ∘ (asbf f1).
 Proof using . intros * f3. cbn-[addf subf]. apply addf_subf. Qed.
 
-Lemma asbf_asbm : ∀ (m : nat) (f : fin (S n)),
+Lemma asbf_asbm : ∀ (m : nat) (f : fin ub),
   asbf (asbm m f) == asbm m ∘ (asbf f).
 Proof using .
   intros m f1 f2. cbn-[addm addf]. rewrite 2 addm_addf. apply addfA.
 Qed.
 
-Lemma asbf_asbf : ∀ f1 f2 : fin (S n),
+Lemma asbf_asbf : ∀ f1 f2 : fin ub,
   asbf (asbf f1 f2) == asbf f1 ∘ (asbf f2).
 Proof using . intros f1 f2 f3. cbn-[addf]. apply addfA. Qed.
 
-Lemma asbf_asbmV : ∀ (m : nat) (f : fin (S n)),
+Lemma asbf_asbmV : ∀ (m : nat) (f : fin ub),
   asbf ((asbm m)⁻¹ f) == (asbm m)⁻¹ ∘ (asbf f).
 Proof using .
   intros m f1 f2. cbn-[subm addf]. rewrite 2 subm_subf, addfC, (addfC f2 f1).
   apply addf_subf.
 Qed.
 
-Lemma asbf_asbfV : ∀ f1 f2 : fin (S n),
+Lemma asbf_asbfV : ∀ f1 f2 : fin ub,
   asbf ((asbf f1)⁻¹ f2) == (asbf f1)⁻¹ ∘ (asbf f2).
 Proof using .
   intros f1 f2 f3. cbn-[subf addf]. rewrite addfC, (addfC f3 f2).
   apply addf_subf.
 Qed.
 
-Lemma asbfV_asbm : ∀ (m : nat) (f : fin (S n)),
+Lemma asbfV_asbm : ∀ (m : nat) (f : fin ub),
   (asbf (asbm m f))⁻¹ == (asbm m)⁻¹ ∘ (asbf f)⁻¹.
 Proof using .
   intros m f1 f2. cbn-[addm subf]. rewrite addm_addf, subm_subf.
   apply subf_addf.
 Qed.
 
-Lemma asbfV_asbf : ∀ f1 f2 : fin (S n),
+Lemma asbfV_asbf : ∀ f1 f2 : fin ub,
   (asbf (asbf f1 f2))⁻¹ == (asbf f1)⁻¹ ∘ (asbf f2)⁻¹.
 Proof using . intros f1 f2 f3. cbn-[addf subf]. apply subf_addf. Qed.
 
-Lemma asbfV_asbmV : ∀ (m : nat) (f : fin (S n)),
+Lemma asbfV_asbmV : ∀ (m : nat) (f : fin ub),
   (asbf ((asbm m)⁻¹ f))⁻¹ == asbm m ∘ (asbf f)⁻¹.
 Proof using .
   intros m f1 f2. cbn-[subm addf]. rewrite addm_addf, subm_subf, addf_subf.
   apply subfA.
 Qed.
 
-Lemma asbfV_asbfV : ∀ f1 f2 : fin (S n),
+Lemma asbfV_asbfV : ∀ f1 f2 : fin ub,
   (asbf ((asbf f1)⁻¹ f2))⁻¹ == asbf f1 ∘ (asbf f2)⁻¹.
 Proof using .
   intros f1 f2 f3. cbn-[subf addf]. rewrite addf_subf. apply subfA.
 Qed.
 
 (* builds the symmetric of f by the center c *)
-Definition symf (c f : fin (S n)) : fin (S n) := addf c (subf c f).
+Definition symf (c f : fin ub) : fin ub := addf c (subf c f).
 
 Definition symf_compat : Proper (equiv ==> equiv ==> equiv) symf := _.
 
-Lemma symfE : ∀ c f : fin (S n), symf c f = addf c (subf c f).
+Lemma symfE : ∀ c f : fin ub, symf c f = addf c (subf c f).
 Proof using . reflexivity. Qed.
 
-Lemma symf2nat : ∀ c f : fin (S n),
-  fin2nat (symf c f) = (S n - f + c + c) mod (S n).
+Lemma symf2nat : ∀ c f : fin ub,
+  fin2nat (symf c f) = (ub - f + c + c) mod ub.
 Proof using .
   intros. rewrite symfE, addf2nat, subf2nat, Nat.add_mod_idemp_r, Nat.add_assoc,
-  (Nat.add_comm _ (_ - _)), Nat.add_assoc. reflexivity. apply Nat.neq_succ_0.
+  (Nat.add_comm _ (_ - _)), Nat.add_assoc. reflexivity. apply neq_ub_0.
 Qed.
 
-Lemma symfI : ∀ c : fin (S n), Preliminary.injective equiv equiv (symf c).
+Lemma symfI : ∀ c : fin ub, Preliminary.injective equiv equiv (symf c).
 Proof using . intros c f1 f2 H. eapply subfI, addfI, H. Qed.
 
-Lemma symfK : ∀ c f : fin (S n), symf c (symf c f) = f.
+Lemma symfK : ∀ c f : fin ub, symf c (symf c f) = f.
 Proof using .
   intros. rewrite 2 symfE, subf_addf, subff, sub0f, oppf_subf. apply subfVK.
 Qed.
 
-Definition symbf (c : fin (S n)) : bijection (fin (S n)) :=
+Definition symbf (c : fin ub) : bijection (fin ub) :=
   cancel_bijection (symf c) _ (@symfI c) (symfK c) (symfK c).
 
-Lemma symbfV : ∀ c : fin (S n), (symbf c)⁻¹ == symbf c.
+Lemma symbfV : ∀ c : fin ub, (symbf c)⁻¹ == symbf c.
 Proof using . intros c f. reflexivity. Qed.
 
-Lemma symf_addf : ∀ (c f1 f2 : fin (S n)),
+Lemma symf_addf : ∀ (c f1 f2 : fin ub),
   symf c (addf f1 f2) = subf (symf c f1) f2.
 Proof using .
   intros. rewrite 2 symfE, subf_addf, addfC, addf_subf, addfC. reflexivity.
 Qed.
 
-Lemma sym0f : ∀ f : fin (S n), symf fin0 f = oppf f.
+Lemma sym0f : ∀ f : fin ub, symf fin0 f = oppf f.
 Proof using . intros. rewrite symfE, add0f. apply sub0f. Qed.
 
-Lemma symf0 : ∀ c : fin (S n), symf c fin0 = addf c c.
+Lemma symf0 : ∀ c : fin ub, symf c fin0 = addf c c.
 Proof using . intros. rewrite symfE, subf0. reflexivity. Qed.
 
-Lemma symff : ∀ f : fin (S n), symf f f = f.
+Lemma symff : ∀ f : fin ub, symf f f = f.
 Proof using . intros. rewrite symfE, subff. apply addf0. Qed.
 
-Definition diff (f1 f2 : fin (S n)) : nat := subf f1 f2.
+Definition diff (f1 f2 : fin ub) : nat := subf f1 f2.
 
 Definition diff_compat : Proper (equiv ==> equiv ==> equiv) diff := _.
 
-Lemma diffE : ∀ f1 f2 : fin (S n), diff f1 f2 = subf f1 f2.
+Lemma diffE : ∀ f1 f2 : fin ub, diff f1 f2 = subf f1 f2.
 Proof using . intros. reflexivity. Qed.
 
-Lemma diffI : ∀ f : fin (S n), Preliminary.injective equiv equiv (diff f).
+Lemma diffI : ∀ f : fin ub, Preliminary.injective equiv equiv (diff f).
 Proof using . intros f1 f2 f3 H. eapply subfI, fin2nat_inj, H. Qed.
 
-Lemma difIf : ∀ f1 : fin (S n),
+Lemma difIf : ∀ f1 : fin ub,
   Preliminary.injective equiv equiv (λ f2, diff f2 f1).
 Proof using . intros f1 f2 f3 H. eapply subIf, fin2nat_inj, H. Qed.
 
-Lemma diff_lt : ∀ f1 f2 : fin (S n), diff f1 f2 < S n.
+Lemma diff_lt : ∀ f1 f2 : fin ub, diff f1 f2 < ub.
 Proof using . intros. apply fin_lt. Qed.
 
-Lemma difff : ∀ f : fin (S n), diff f f = 0.
+Lemma difff : ∀ f : fin ub, diff f f = 0.
 Proof using . intros. rewrite diffE, subff. apply fin02nat. Qed.
 
-Lemma dif0f : ∀ f : fin (S n), diff fin0 f = oppf f.
+Lemma dif0f : ∀ f : fin ub, diff fin0 f = oppf f.
 Proof using . intros. rewrite diffE, sub0f. reflexivity. Qed.
 
-Lemma diff0 : ∀ f : fin (S n), diff f fin0 = f.
+Lemma diff0 : ∀ f : fin ub, diff f fin0 = f.
 Proof using . intros. rewrite diffE, subf0. reflexivity. Qed.
 
-Lemma diff_neq : ∀ f1 f2 : fin (S n), f1 ≠ f2 -> 0 < diff f1 f2.
+Lemma diff_neq : ∀ f1 f2 : fin ub, f1 ≠ f2 -> 0 < diff f1 f2.
 Proof using .
   intros * H. apply neq_0_lt. intros Habs. elim H. eapply diffI.
   rewrite (difff f1). apply Habs.
 Qed.
 
-Lemma symf_addm_diff : ∀ c f : fin (S n), symf c f = addm c (diff c f).
+Lemma symf_addm_diff : ∀ c f : fin ub, symf c f = addm c (diff c f).
 Proof using . intros. rewrite diffE, addm_addf, mod2finK. reflexivity. Qed.
 
-Lemma oppm_diff : ∀ f1 f2 : fin (S n), oppm (diff f1 f2) = subf f2 f1.
+Lemma oppm_diff : ∀ f1 f2 : fin ub, oppm (diff f1 f2) = subf f2 f1.
 Proof using . intros. rewrite diffE, oppm_oppf, mod2finK. apply oppf_subf. Qed.
 
 End mod2fin.