proposition: Lemma hrndG_N : forall x, ( forall b, rdir (rnd_record_mk (ZtoN (Zfloor x)) b true) = b ) -> hrndG x = Znearest (fun x => rdir (rnd_record_mk (ZtoN x) true false)) x.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx1. destruct (good_rdir (ZtoN (Zfloor x))) as (Hx2, _). unfold hrndG, hrndG_aux. destruct (inbetween_spec _ _ x (bracket_aux _)) as [Hx4|l Hx4 Hx5]. rewrite Hx2. rewrite Hx4 at 2. rewrite Zrnd_IZR... unfold Znearest. rewrite Rcompare_floor_ceil_middle with (1 := Rlt_not_eq _ _ (proj1 Hx4)). rewrite Rcompare_middle. rewrite Zceil_floor_neq with (1 := Rlt_not_eq _ _ (proj1 Hx4)). rewrite plus_IZR. rewrite Hx5. now case l ; rewrite ?Hx1, ?Hx2. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux