diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZAdd.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 202875b8a..8bed3027f 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -30,6 +30,11 @@ intros n m; nzinduct n. now nzsimpl. intro. nzsimpl. now rewrite succ_inj_wd. Qed. +Theorem add_succ_comm : forall n m, S n + m == n + S m. +Proof. +intros n m. now rewrite add_succ_r, add_succ_l. +Qed. + Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. @@ -82,6 +87,11 @@ Proof. intros n m p q. rewrite (add_comm p). apply add_shuffle1. Qed. +Theorem add_shuffle3 : forall n m p, n + (m + p) == m + (n + p). +Proof. +intros n m p. now rewrite add_comm, <- add_assoc, (add_comm p). +Qed. + Theorem sub_1_r : forall n, n - 1 == P n. Proof. intro n; now nzsimpl'. |