proposition: Lemma flt_le : forall x : R, forall xn zn : positive, FLT x xn -> (Zpos xn <= Zpos zn)%Z -> FLT x zn.
proof: Proof. intros x xn zn (xf,(Hx1,Hx2)) H. exists xf. split. exact Hx1. apply Z.lt_le_trans with (1 := Hx2). apply le_IZR. change (IZR (Zpower radix2 (Zpos xn)) <= IZR (Zpower radix2 (Zpos zn)))%R. apply IZR_le. now apply Zpower_le. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux Defs Digits Float_prop Generic_fmt FIX FLX) Gappa_definitions Gappa_dyadic