diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZPlus.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZPlus.v | 58 |
1 files changed, 29 insertions, 29 deletions
diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v index 673b819ba..6fb72ed4a 100644 --- a/theories/Numbers/NatInt/NZPlus.v +++ b/theories/Numbers/NatInt/NZPlus.v @@ -17,69 +17,69 @@ Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig). Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod. Open Local Scope NatIntScope. -Theorem NZplus_0_r : forall n : NZ, n + 0 == n. +Theorem NZadd_0_r : forall n : NZ, n + 0 == n. Proof. -NZinduct n. now rewrite NZplus_0_l. -intro. rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd. +NZinduct n. now rewrite NZadd_0_l. +intro. rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. Qed. -Theorem NZplus_succ_r : forall n m : NZ, n + S m == S (n + m). +Theorem NZadd_succ_r : forall n m : NZ, n + S m == S (n + m). Proof. intros n m; NZinduct n. -now do 2 rewrite NZplus_0_l. -intro. repeat rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd. +now do 2 rewrite NZadd_0_l. +intro. repeat rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. Qed. -Theorem NZplus_comm : forall n m : NZ, n + m == m + n. +Theorem NZadd_comm : forall n m : NZ, n + m == m + n. Proof. intros n m; NZinduct n. -rewrite NZplus_0_l; now rewrite NZplus_0_r. -intros n. rewrite NZplus_succ_l; rewrite NZplus_succ_r. now rewrite NZsucc_inj_wd. +rewrite NZadd_0_l; now rewrite NZadd_0_r. +intros n. rewrite NZadd_succ_l; rewrite NZadd_succ_r. now rewrite NZsucc_inj_wd. Qed. -Theorem NZplus_1_l : forall n : NZ, 1 + n == S n. +Theorem NZadd_1_l : forall n : NZ, 1 + n == S n. Proof. -intro n; rewrite NZplus_succ_l; now rewrite NZplus_0_l. +intro n; rewrite NZadd_succ_l; now rewrite NZadd_0_l. Qed. -Theorem NZplus_1_r : forall n : NZ, n + 1 == S n. +Theorem NZadd_1_r : forall n : NZ, n + 1 == S n. Proof. -intro n; rewrite NZplus_comm; apply NZplus_1_l. +intro n; rewrite NZadd_comm; apply NZadd_1_l. Qed. -Theorem NZplus_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p. +Theorem NZadd_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p. Proof. intros n m p; NZinduct n. -now do 2 rewrite NZplus_0_l. -intro. do 3 rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd. +now do 2 rewrite NZadd_0_l. +intro. do 3 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. Qed. -Theorem NZplus_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q). +Theorem NZadd_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q). Proof. intros n m p q. -rewrite <- (NZplus_assoc n m (p + q)). rewrite (NZplus_comm m (p + q)). -rewrite <- (NZplus_assoc p q m). rewrite (NZplus_assoc n p (q + m)). -now rewrite (NZplus_comm q m). +rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_comm m (p + q)). +rewrite <- (NZadd_assoc p q m). rewrite (NZadd_assoc n p (q + m)). +now rewrite (NZadd_comm q m). Qed. -Theorem NZplus_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p). +Theorem NZadd_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p). Proof. intros n m p q. -rewrite <- (NZplus_assoc n m (p + q)). rewrite (NZplus_assoc m p q). -rewrite (NZplus_comm (m + p) q). now rewrite <- (NZplus_assoc n q (m + p)). +rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_assoc m p q). +rewrite (NZadd_comm (m + p) q). now rewrite <- (NZadd_assoc n q (m + p)). Qed. -Theorem NZplus_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m. +Theorem NZadd_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m. Proof. intros n m p; NZinduct p. -now do 2 rewrite NZplus_0_l. -intro p. do 2 rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. Qed. -Theorem NZplus_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. +Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. Proof. -intros n m p. rewrite (NZplus_comm n p); rewrite (NZplus_comm m p). -apply NZplus_cancel_l. +intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). +apply NZadd_cancel_l. Qed. Theorem NZminus_1_r : forall n : NZ, n - 1 == P n. |