More arithmetic theorems

In ssrnat:
- some trivial results in ssrnat `addnKC`, `ltn_predl`, `ltn_predr`, `ltn_subr` and `predn_sub`
- theorems about `n <=/< p +/- m`  and `m +/- n <=/< p`
  `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`,
  `leq_subCl`, `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and `ltn_subCl`

In div:
- theorems about the euclidean division of additions and subtraction,
  + without preconditions of divisibility:
    `edivnD`, `edivnB`, `divnD`, `divnB`, `modnD`, `modnB`
  + with divisibility of one argument:
    `divnDMl`, `divnMBl`, `divnBMl`, `divnBl` and `divnBr`
  + specialization of the former theorems for .+1 and .-1:
    `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and `modn_pred`

0 files changed, 0 insertions, 0 deletions