proposition: Lemma generic_format_pred_pos : forall x, F x -> (0 < x)%R -> F (pred_pos x).
proof: Proof. intros x Fx Zx. unfold pred_pos; case Req_bool_spec; intros H. now apply generic_format_pred_aux2. now apply generic_format_pred_aux1. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop