diff options
| author |  jadep <jadep@mit.edu> | 2019-03-12 13:06:56 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-03-25 06:13:45 -0400 |
| commit | b1bdefa45c0fa9786a8f916981a67ac5a4961eb0 (patch) | |
| tree | 3258749dd759d170d1133458afe7fce11ccfa5b7 /src/Util/ZUtil/Divide.v | |
| parent | 684d356bcb81ca36314cd7864c62a1d97af4ea99 (diff) | |
Move some lemmas to appropriate places
Diffstat (limited to 'src/Util/ZUtil/Divide.v')
| -rw-r--r-- | src/Util/ZUtil/Divide.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Divide.v b/src/Util/ZUtil/Divide.v index 8609db5ad..b49530194 100644 --- a/src/Util/ZUtil/Divide.v +++ b/src/Util/ZUtil/Divide.v @@ -33,4 +33,11 @@ Module Z. apply Zmod_divide; omega || auto. } Qed. + + Lemma divide_pow_le b n m : 0 <= n <= m -> (b ^ n | b ^ m). + Proof. + intros. replace m with (n + (m - n)) by ring. + rewrite Z.pow_add_r by lia. + apply Z.divide_factor_l. + Qed. End Z. |