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