diff options
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 5c65148c0..344eb40c9 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -10,7 +10,7 @@ Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify. -Hint Rewrite sub_diag add_0_l add_0_r sub_0_r : natsimplify. +Hint Rewrite sub_diag add_0_l add_0_r sub_0_r sub_succ : natsimplify. Local Open Scope nat_scope. @@ -66,7 +66,7 @@ Proof. reflexivity. Qed. -Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. +Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. Proof. intros; apply Nat.mod_small. destruct m; try omega; rewrite Nat.pred_succ; auto. @@ -291,3 +291,15 @@ Proof. apply f_equal, le_unique. Qed. Hint Rewrite le_dec_pred_plus_same : natsimplify. + +Lemma minus_S_diag x : (S x - x = 1)%nat. +Proof. omega. Qed. +Hint Rewrite minus_S_diag : natsimplify. + +Lemma min_idempotent_S_l x : min (S x) x = x. +Proof. omega *. Qed. +Hint Rewrite min_idempotent_S_l : natsimplify. + +Lemma min_idempotent_S_r x : min x (S x) = x. +Proof. omega *. Qed. +Hint Rewrite min_idempotent_S_r : natsimplify. |