proposition: Theorem succ_gt_ge : forall x y, (y <> 0)%R -> (x <= y)%R -> (x < succ y)%R.
proof: Proof. intros x y Zy Hxy. apply Rle_lt_trans with (1 := Hxy). now apply succ_gt_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop