diff options
| author | Cyril Cohen | 2019-10-25 01:56:42 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-25 02:00:48 +0200 |
| commit | 30e7fe9f41fc7d5c4741257914c78c183926f02c (patch) | |
| tree | 8212678bc0cc969a27f30624d19a065f66dbc017 /docs | |
| parent | 4b9efb7e411bfd1e9618fa94f61fb065af84e394 (diff) | |
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`
Diffstat (limited to 'docs')
0 files changed, 0 insertions, 0 deletions