Remove abs_ceil_ge

[pi8027]

Motivation for this change

math-comp/math-comp#1515 (comment)

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[pi8027]

Perhaps, one thing you missed was the lemmas for going back and forth between inequations over reals and integers (including nat), e.g., truncn_le_nat, floor_ge_int, and floor_lt_int.

Ideally, this kind of proof should be fully automated, since mixed real-integer linear arithmetic (with floor, ceil, and truncn) is decidable.