Collect #Ceil conditions introduced by equations with partial functions

[jberthold]

While #3779 is concerned with rewrite rules (and relatively straightforward), collecting #Ceil conditions introduced by simplifications and function-defining equations is complex because of

• possible recursive evaluation of side conditions - the collected #Ceil conditions may have to be discarded if the recursive caller ends up failing for other reasons
• when the #Ceil condition comes from simplifying a rewrite rule side condition, the negated condition becomes a remainder and rewriting needs to proceed with this remainder added to the assumed condition (unless it can be pruned - has to be simplified "soon"). This potentially leads to branching.

This extension is expected to considerably reduce the fall-back cases because many more simplifications can be applied.

[jberthold]

See off-site notes for a longer elaboration of this topic