proposition: Theorem new_location_correct : forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location k l).
proof: Proof. intros x k l Hk Hx. unfold new_location. generalize (refl_equal nb_steps) (Z.le_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)). pattern nb_steps at 2 3 5 ; case nb_steps. now intros _. intros [p|p|] Hp _. apply new_location_odd_correct with (2 := Hk) (3 := Hx). now rewrite Hp. apply new_location_even_correct with (2 := Hk) (3 := Hx). now rewrite Hp. now rewrite Hp in Hnb_steps. now intros p _. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop