proposition: Lemma Zmax_inf_l : forall m n : Z, (n <= m)%Z -> Z.max m n = m.
proof: Proof. intros m n H. generalize (Z.le_ge _ _ H). unfold Z.max, Z.ge. case (m ?= n)%Z ; intros ; try exact (refl_equal _). elim H0. exact (refl_equal _). Qed.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round