proposition: Lemma roundUP_eq : forall x, rndG roundUP x = Zceil x.
proof: Proof. intros x. simpl. unfold rndG. case Rcompare_spec ; intros H. rewrite hrndG_DN ; try easy. apply roundUP. rewrite H. apply sym_eq. apply Zceil_IZR. rewrite hrndG_UP ; try easy. apply roundUP. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux