proposition: Theorem fix_subset : forall x : R, forall xn zn : Z, FIX x xn -> Zle_bool zn xn = true -> FIX x zn.
proof: Proof. intros x xn zn Hx Hb. apply fix_le with (1 := Hx). now apply Zle_bool_imp_le. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux