let rec build_periodicity_cstr iof_c_n_j' (nbones_c_n_u, nbones_c_n_v) =
match iof_c_n_j' with
| Size _ -> assert false
| Iof (c_n, j') ->
assert (j' > nbones_c_n_u + nbones_c_n_v);
let j'_v = j' - nbones_c_n_u in
let j_v =
if j'_v mod nbones_c_n_v = 0 then nbones_c_n_v
else j'_v mod nbones_c_n_v
in
let j = nbones_c_n_u + j_v in
let l =
if j'_v mod nbones_c_n_v = 0 then (j'_v - nbones_c_n_v) / nbones_c_n_v
else j'_v / nbones_c_n_v
in
assert (j' = j + l * nbones_c_n_v);
Eq ([ 1, Iof (c_n, j');
-1, Iof (c_n, j);
-l, Size c_n; ], 0)