diff options
Diffstat (limited to 'src/Util/ZUtil/ZSimplify/Simple.v')
| -rw-r--r-- | src/Util/ZUtil/ZSimplify/Simple.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v index 94fa05e1a..b176c0b21 100644 --- a/src/Util/ZUtil/ZSimplify/Simple.v +++ b/src/Util/ZUtil/ZSimplify/Simple.v @@ -13,6 +13,9 @@ Module Z. Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1. Proof. apply Z.pow_1_l; lia. Qed. Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_0_l_Zpos a : 0^Zpos a = 0. + Proof. apply Z.pow_0_l; lia. Qed. + Hint Rewrite pow_0_l_Zpos : zsimplify_fast zsimplify_const zsimplify. Lemma sub_same_minus (x y : Z) : x - (x - y) = y. Proof. lia. Qed. |