diff options
| author | emakarov | 2007-11-14 19:47:46 +0000 |
|---|---|---|
| committer | emakarov | 2007-11-14 19:47:46 +0000 |
| commit | 87bfa992d0373cd1bfeb046f5a3fc38775837e83 (patch) | |
| tree | 5a222411c15652daf51a6405e2334a44a9c95bea /theories/Numbers/NatInt/NZTimes.v | |
| parent | d04ad26f4bb424581db2bbadef715fef491243b3 (diff) | |
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
Diffstat (limited to 'theories/Numbers/NatInt/NZTimes.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZTimes.v | 18 |
1 files changed, 9 insertions, 9 deletions
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. |