diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZUtil.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1a7b54d84..1e0ed36e4 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1235,6 +1235,31 @@ Module Z. Proof. lia. Qed. Hint Rewrite simplify_twice_sub_add : zsimplify. + Lemma simplify_once_add_add_add x y z : x + y + (x + z) = 2 * x + y + z. + Proof. lia. Qed. + Hint Rewrite simplify_once_add_add_add : zsimplify. + Lemma simplify_once_add_add_sub x y z : x + y + (x - z) = 2 * x + y - z. + Proof. lia. Qed. + Hint Rewrite simplify_once_add_add_sub : zsimplify. + Lemma simplify_once_add_sub_add x y z : x + y - (x + z) = y - z. + Proof. lia. Qed. + Hint Rewrite simplify_once_add_sub_add : zsimplify. + Lemma simplify_once_add_sub_sub x y z : x + y - (x - z) = y + z. + Proof. lia. Qed. + Hint Rewrite simplify_once_add_sub_sub : zsimplify. + Lemma simplify_once_sub_add_add x y z : x - y + (x + z) = 2 * x - y + z. + Proof. lia. Qed. + Hint Rewrite simplify_once_sub_add_add : zsimplify. + Lemma simplify_once_sub_add_sub x y z : x - y + (x - z) = 2 * x - y - z. + Proof. lia. Qed. + Hint Rewrite simplify_once_sub_add_sub : zsimplify. + Lemma simplify_once_sub_sub_add x y z : x - y - (x + z) = -y - z. + Proof. lia. Qed. + Hint Rewrite simplify_once_sub_sub_add : zsimplify. + Lemma simplify_once_sub_sub_sub x y z : x - y - (x - z) = z - y. + Proof. lia. Qed. + Hint Rewrite simplify_once_sub_sub_sub : zsimplify. + Section equiv_modulo. Context (N : Z). Definition equiv_modulo x y := x mod N = y mod N. |