proposition: Theorem flt_subset : forall x : R, forall xn zn : positive, FLT x xn -> Zle_bool (Zpos xn) (Zpos zn) = true -> FLT x zn.
proof: Proof. intros x xn zn Hx Hb. apply flt_le with (1 := Hx). now apply Zle_bool_imp_le. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux