aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NatUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/NatUtil.v')
-rw-r--r--src/Util/NatUtil.v20
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 83375f99a..6d4efd9f4 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -64,6 +64,26 @@ Proof.
reflexivity.
Qed.
+Lemma div_add_l' : forall a b c, a <> 0 -> (a * b + c) / a = b + c / a.
+Proof.
+ intros; rewrite Nat.mul_comm; auto using div_add_l.
+Qed.
+
+Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
+Proof.
+ intros; rewrite Nat.add_comm; auto using mod_add.
+Qed.
+
+Lemma mod_add_l' : forall a b c, b <> 0 -> (b * a + c) mod b = c mod b.
+Proof.
+ intros; rewrite Nat.mul_comm; auto using mod_add_l.
+Qed.
+
+Lemma mod_div_eq0 : forall a b, b <> 0 -> a mod b / b = 0.
+Proof.
+ intros; apply Nat.div_small, mod_bound_pos; omega.
+Qed.
+
Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2).
Proof.
assert (4 <> 0) as ne40 by omega.