diff options
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: |