proposition: Lemma Zfloor_plus: forall (n:Z) y, (Zfloor (IZR n+y) = n + Zfloor y)%Z.
proof: Proof. intros n y; unfold Zfloor. unfold Zminus; rewrite Zplus_assoc; f_equal. apply sym_eq, tech_up. rewrite plus_IZR. apply Rplus_lt_compat_l. apply archimed. rewrite plus_IZR, Rplus_assoc. apply Rplus_le_compat_l. apply Rplus_le_reg_r with (-y)%R. ring_simplify (y+1+-y)%R. apply archimed. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations