proposition: Theorem Zaway_floor : forall x, (x <= 0)%R -> Zaway x = Zfloor x.
proof: Proof. intros x Hx. unfold Zaway. case Rlt_bool_spec ; intro H. apply refl_equal. rewrite (Rle_antisym _ _ Hx H). rewrite Zfloor_IZR. apply Zceil_IZR. Qed.
imports: Coq(Psatz Reals ZArith) Zaux