diff options
| -rw-r--r-- | src/Util/ZUtil.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 7a654d48f..1a7b54d84 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1227,6 +1227,14 @@ Module Z. Proof. intros; symmetry; apply Zminus_mod_idemp_r; assumption. Qed. Hint Rewrite sub_mod_r_push using solve [ NoZMod | lia ] : push_Zmod. + Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y. + Proof. lia. Qed. + Hint Rewrite simplify_twice_sub_sub : zsimplify. + + Lemma simplify_twice_sub_add x y : 2 * x - (x + y) = x - y. + Proof. lia. Qed. + Hint Rewrite simplify_twice_sub_add : zsimplify. + Section equiv_modulo. Context (N : Z). Definition equiv_modulo x y := x mod N = y mod N. |