various cleanups and simplifications in util

Pierre's cleanups from !190, minus the TODO annotations.

CC: @proux

assigned to @bbb

I ran out of time for now. I'll try to get this finished and merged in the next week or so.

mentioned in merge request !190

To be clear, I'll take care of the Prosa style cleanups and do not suggest that the MathComp PR should look like this.

added 5 commits

• c35a5da4 - fixup! Prepare subdnD for MathComp PR
• 7e73cb4b - fixup! Simplify proof of sum_notin_rem_eqn
• 5bfe7f2f - fixup! Simplify proof of leq_sum_sub_uniq
• bd181e48 - util.sum: adjust identation style
• f642885b - util.sum: fix comments

Compare with previous version

marked this merge request as draft from c35a5da4

added 2 commits

• 89b9f722 - fixup! Remove sum0
• bc89e5cb - fixup! Simplify proof of sum_majorant_eqn

Compare with previous version

resolved all threads

added 1 commit

• 802efc7f - util.sum: clean up organization and add some comments

Compare with previous version

added 19 commits

• bb76b8bd - Prepare subdnD for MathComp PR
• 010ef216 - Prepare leq_subRL_impl for MathComp PR
• 0e8d85e0 - Remove exists_or_not_add_mul_cases
• 8ff12f1c - Remove add_mul_diff
• 162e01f4 - Rewrite 2 proofs in more ssreflect style
• 4a9a0cfc - Generalize and simplify proof of sum_nat_eq0_nat
• 594d4da6 - Simplify sum_nat_gt0
• 2d72fd86 - Simplify proof of sum_notin_rem_eqn
• e1d58324 - Simplify proof of sum_majorant_constant
• 9a537fa3 - Simplify proof of sum_pred_diff
• fb9eb1f3 - Simplify proof of leq_sum_sub_uniq
• 1c1a8bf9 - Simplify proof of {l,}eq_sum_seq
• d15b1e83 - Simplify proof of leq_sum_seq_pred
• a9431bf0 - Simplify proof of sumnB_nat
• fd7baf22 - Remove sum_seq_cond_gt0P
• e6205fed - Simplify proof of sum_majorant_eqn
• 9e195050 - Remove sum0
• fb3e19b5 - Simplify proof of sum_of_ones
• 771bdee0 - util.sum: clean up organization and add some comments

Compare with previous version

marked this merge request as ready

added 1 commit

• 45391d62 - reorganize `util.sum` and add some comments

Compare with previous version

enabled an automatic merge when the pipeline for 45391d62 succeeds

merged