From 87bfa992d0373cd1bfeb046f5a3fc38775837e83 Mon Sep 17 00:00:00 2001
From: emakarov
Date: Wed, 14 Nov 2007 19:47:46 +0000
Subject: Update on Numbers; renamed ZOrder.v to ZLt to remove clash with
 ZArith/Zorder on MacOS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZTimes.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'theories/Numbers/NatInt/NZTimes.v')

diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v
index e0d1f63501..20bd3cdc61 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -17,20 +17,20 @@ Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
-Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0.
+Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0.
 Proof.
 NZinduct n.
-now rewrite NZtimes_0_r.
-intro. rewrite NZtimes_succ_r. now rewrite NZplus_0_r.
+now rewrite NZtimes_0_l.
+intro. rewrite NZtimes_succ_l. now rewrite NZplus_0_r.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m.
+Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
 Proof.
-intros n m; NZinduct m.
-do 2 rewrite NZtimes_0_r; now rewrite NZplus_0_l.
-intro m. do 2 rewrite NZtimes_succ_r. do 2 rewrite NZplus_succ_r.
-rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) n m).
-rewrite (NZplus_comm n m). rewrite NZplus_assoc.
+intros n m; NZinduct n.
+do 2 rewrite NZtimes_0_l; now rewrite NZplus_0_l.
+intro n. do 2 rewrite NZtimes_succ_l. do 2 rewrite NZplus_succ_r.
+rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) m n).
+rewrite (NZplus_comm m n). rewrite NZplus_assoc.
 now rewrite NZplus_cancel_r.
 Qed.
 
-- 
cgit v1.2.3