diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-25 21:04:23 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-25 21:04:23 -0400 |
| commit | ea9397e3da37f35d088488be141cb18cc38ea11b (patch) | |
| tree | 2cb1f857951e2388b79253cb5be123f2b0d383fb /src/Util/NatUtil.v | |
| parent | e880359898151f81383844b602df0c6df7f88ad1 (diff) | |
A couple new util lemmas
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 1c144281b..84fbb11eb 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -64,6 +64,11 @@ Proof. reflexivity. Qed. +Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = Init.Nat.pred m. +Proof. + intros; apply Nat.mod_small; omega. +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. |