From b1bdefa45c0fa9786a8f916981a67ac5a4961eb0 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 13:06:56 -0400 Subject: Move some lemmas to appropriate places --- src/Util/ZUtil/Divide.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/ZUtil/Divide.v') 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. -- cgit v1.2.3