proposition: Lemma roundZR_eq : forall x, rndG roundZR x = Ztrunc x.
proof: Proof. intros x. simpl. unfold rndG, Ztrunc. destruct (Rlt_bool_spec x 0) as [Hx|[Hx|Hx]]. rewrite Rcompare_Lt with (1 := Hx). rewrite hrndG_DN ; try easy. apply roundZR. rewrite Rcompare_Gt with (1 := Hx). rewrite hrndG_DN ; try easy. apply roundZR. rewrite <- Hx. rewrite Rcompare_Eq with (1 := refl_equal _). apply sym_eq. apply Zfloor_IZR. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux