From c7123e2a55c2751e83518c0866baac254f51ec3d Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 18 Jul 2016 08:37:34 -0400 Subject: Added lemmas to ZUtil and NatUtil (for Testbit) --- src/Util/NatUtil.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src/Util/NatUtil.v') 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. -- cgit v1.2.3