proposition: Lemma hrndG_UP : forall x, rdir (rnd_record_mk (ZtoN (Zfloor x)) false true) = true -> hrndG x = Zceil x.
proof: Proof. intros x Hx1. destruct (good_rdir (ZtoN (Zfloor x))) as (Hx2, (Hx3, Hx4)). rewrite Hx1 in Hx3. destruct Hx3 as [Hx3|Hx3] ; try easy. rewrite Hx3 in Hx4. destruct Hx4 as [Hx4|Hx4] ; try easy. unfold hrndG, hrndG_aux. destruct (inbetween_spec _ _ x (bracket_aux _)) as [H|l H1 H2]. rewrite Hx2. rewrite H at 2. now rewrite Zceil_IZR. now case l ; rewrite ?Hx1, ?Hx3, ?Hx4. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux