proposition: Theorem succ_lt : forall x y, F x -> F y -> (x < y)%R -> (succ x < succ y)%R.
proof: Proof. intros x y Fx Fy Hxy. apply Rnot_le_lt. intros H. apply Rgt_not_le with (1 := Hxy). now apply succ_le_inv. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop