Fix step boundaries in fold_range_step_by

[mamonet]

I run into case where index boundaries need to be precise for fold_range_step_by, let's consider the following case

Rust_primitives.Hax.Folds.fold_range_step_by 0ul
  32ul
  (sz 4)
  (fun sampled_i16s temp_1_ ->
      true)
  sampled_i16s
  (fun sampled_i16s outcome_set ->
      sampled_i16s)

The steps are the following [0, 4, 8, 12, 16, 20, 24, 28] so the boundary for index is i <= 28 but by default I get i < 32 by the condition v i < v end_ in fold_range_step_by, I adjusted that with proper condition in this PR.

[karthikbhargavan]

This is only used in ML-KEM for now. I feel there must be a better way of writing this condition, but let's get it in and iterate.

[mamonet]

This is only used in ML-KEM for now. I feel there must be a better way of writing this condition, but let's get it in and iterate.

I think Lucas was thinking about proper condition by having this commented out line // /\ i % v step == v start % v step, while that condition is true, and I think it should be there I am not sure if it affects the index boundary which what I need for MLKEM now.