proposition: Lemma hrndG_pos : forall x, (0 <= x)%R -> (0 <= hrndG x)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. rewrite <- (Zrnd_IZR hrndG 0). apply Zrnd_le... Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux