diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZDivEucl.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index e1802dbeeb..954b89150a 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -268,6 +268,11 @@ Proof. intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag. Qed. +Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b. +Proof. + intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul. +Qed. + (** * Order results about mod and div *) (** A modulo cannot grow beyond its starting point. *) |