proposition: Lemma roundDN_eq : forall x, rndG roundDN x = Zfloor x.
proof: Proof. intros x. simpl. unfold rndG. case Rcompare_spec ; intros H. rewrite hrndG_UP. unfold Zceil. rewrite Ropp_involutive. apply Z.opp_involutive. apply roundDN. apply refl_equal. rewrite H. apply sym_eq. apply Zfloor_IZR. rewrite hrndG_DN ; try easy. apply roundDN. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux