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