proposition: Lemma middle_odd : forall k, (2 * k + 1 = nb_steps)%Z -> (((start + IZR k * step) + (start + IZR (k + 1) * step))/2 = start + IZR nb_steps /2 * step)%R.
proof: Proof. intros k Hk. rewrite <- Hk. rewrite 2!plus_IZR, mult_IZR. simpl. field. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop