diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-03 01:04:46 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-03 01:04:46 -0400 |
commit | 5abe840c27713771665edd0a3beb040fccfbf041 (patch) | |
tree | ede40e0555684e78358735d5732946a722b7e394 /src | |
parent | a0fab645d1fd01e56c7d6b78178d77eaddbd02e6 (diff) |
Add Zpow_sub_1_nat_pow
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/ZUtil.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 01e125e00..973c2685d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -80,6 +80,19 @@ Module Z. Hint Rewrite pow_Zpow : push_Zof_nat. Hint Rewrite <- pow_Zpow : pull_Zof_nat. + Lemma Zpow_sub_1_nat_pow a v + : (Z.pos a^Z.of_nat v - 1 = Z.of_nat (Z.to_nat (Z.pos a)^v - 1))%Z. + Proof. + rewrite <- (Z2Nat.id (Z.pos a)) at 1 by lia. + change 2%Z with (Z.of_nat 2); change 1%Z with (Z.of_nat 1); + autorewrite with pull_Zof_nat. + rewrite Nat2Z.inj_sub + by (change 1%nat with (Z.to_nat (Z.pos a)^0)%nat; apply Nat.pow_le_mono_r; simpl; lia). + reflexivity. + Qed. + Hint Rewrite Zpow_sub_1_nat_pow : pull_Zof_nat. + Hint Rewrite <- Zpow_sub_1_nat_pow : push_Zof_nat. + Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), (a | b * (a / c)) -> (c | a) -> (c | b). Proof. |