Ohad Kammar 0c1a124704 Division theorem (#695) ... Division Theorem. For every natural number `x` and positive natural number `n`, there is a unique decomposition: `x = q*n + r` with `q`,`r` natural and `r` < `n`. `q` is the quotient when dividing `x` by `n` `r` is the remainder when dividing `x` by `n`. This commit adds a proof for this fact, in case we want to reason about modular arithmetic (for example, when dealing with binary representations). A future, more systematic, development could perhaps follow: @clayrat 's (idris1) port of Coq's binary arithmetics: https://github.com/sbp/idris-bi/blob/master/src/Data/Bin/DivMod.idr https://github.com/sbp/idris-bi/blob/master/src/Data/Biz/DivMod.idr https://github.com/sbp/idris-bi/blob/master/src/Data/BizMod2/DivMod.idr In the process, it bulks up the stdlib with: + a generic PreorderReasoning module for arbitrary preorders, analogous for the equational reasoning module + some missing facts about Nat operations. + Refactor some Nat order properties using a 'reflect' function Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk> Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>		2020-10-06 13:09:02 +01:00
..
Generic.idr	Division theorem (#695)	2020-10-06 13:09:02 +01:00