proposition: Theorem Zaway_ceil : forall x, (0 <= x)%R -> Zaway x = Zceil x.
proof: Proof. intros x Hx. unfold Zaway. case Rlt_bool_spec ; intro H. elim Rlt_irrefl with x. now apply Rlt_le_trans with R0. apply refl_equal. Qed.
imports: Coq(Psatz Reals ZArith) Zaux