proposition: Theorem Zaway_le : forall x y, (x <= y)%R -> (Zaway x <= Zaway y)%Z.
proof: Proof. intros x y Hxy. unfold Zaway at 1. case Rlt_bool_spec ; intro Hx. unfold Zaway. case Rlt_bool_spec ; intro Hy. now apply Zfloor_le. apply le_IZR. apply Rle_trans with 0%R. apply Rlt_le. apply Rle_lt_trans with (2 := Hx). apply Zfloor_lb. apply Rle_trans with (1 := Hy). apply Zceil_ub. rewrite Zaway_ceil. now apply Zceil_le. now apply Rle_trans with x. Qed.
imports: Coq(Psatz Reals ZArith) Zaux