proposition: Lemma roundNA_eq : forall x, rndG roundNA x = rndNA x.
proof: Proof. apply roundN_eq ; intros m Hm r s ; simpl. rewrite Zle_bool_false. now rewrite orb_comm, andb_comm. lia. rewrite Zle_bool_true with (1 := Hm). now rewrite orb_comm, andb_comm. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux