proposition: Lemma roundNE_eq : forall x, rndG roundNE x = rndNE x.
proof: Proof. apply roundN_eq ; intros m Hm r s ; unfold roundNE, GrndNE ; simpl ; apply (f_equal (fun v => r && (s || negb v))). rewrite Z.even_opp, Z.even_add. now destruct m as [|[m|m|]|]. now destruct m as [|[m|m|]|]. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux