proposition: Theorem pred_ge_0 : forall x, (0 < x)%R -> F x -> (0 <= pred x)%R.
proof: Proof. intros x Zx Fx. rewrite pred_eq_pos. now apply pred_pos_ge_0. now left. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop