diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:51:10 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 14:51:10 +0200 |
| commit | 4d54945d8df4b9b3c0bca17f5bd4d391d7012c8f (patch) | |
| tree | 98db76c7b92e66cdbb5ab51147756becaef823ab /theories/Numbers | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
| parent | 8eb6370b94af56b94d2645aa4eaab5915341b961 (diff) | |
Merge PR #845: Add Z.mod_div lemma to standard library.
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 8 |
3 files changed, 24 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index ce49877e4..967b68d36 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -602,6 +602,14 @@ Proof. apply div_mod; order. Qed. +Lemma mod_div: forall a b, b~=0 -> + a mod b / b == 0. +Proof. + intros a b Hb. + rewrite div_small_iff by assumption. + auto using mod_always_pos. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index ca6197002..a9077127e 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -650,6 +650,14 @@ Proof. apply div_mod; order. Qed. +Lemma mod_div: forall a b, b~=0 -> + a mod b / b == 0. +Proof. + intros a b Hb. + rewrite div_small_iff by assumption. + auto using mod_bound_or. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 46c36015d..bbb8ad5ae 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -622,6 +622,14 @@ Proof. apply quot_rem; order. Qed. +Lemma rem_quot: forall a b, b~=0 -> + a rem b ÷ b == 0. +Proof. + intros a b Hb. + rewrite quot_small_iff by assumption. + auto using rem_bound_abs. +Qed. + (** A last inequality: *) Theorem quot_mul_le: |