diff options
Diffstat (limited to 'theories/Numbers/Integer/NatPairs/ZPairsTimes.v')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsTimes.v | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v index b72847c089..47bf8cd082 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v @@ -3,9 +3,9 @@ Require Import NTimes. Require Export ZTimes. Require Export ZPairsPlus. -Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature. -Module Export ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *) -Module Import NTimesPropertiesModule := NTimesProperties NTimesModule. +Module NatPairsTimes (Import NTimesMod : NTimesSig) <: ZTimesSignature. +Module Export ZPlusModule := NatPairsPlus NTimesMod.NPlusMod. (* "NTimesMod." is optional *) +Module Import NTimesPropertiesModule := NTimesPropFunct NTimesMod. Open Local Scope NatScope. Definition times (n m : Z) := @@ -41,15 +41,22 @@ intro n; unfold times, E; simpl. repeat rewrite times_0_r. now rewrite plus_assoc. Qed. -Theorem times_S : forall n m, n * (S m) == n * m + n. +Theorem times_succ : forall n m, n * (S m) == n * m + n. Proof. intros n m; unfold times, S, E; simpl. -do 2 rewrite times_S_r. ring. +do 2 rewrite times_succ_r. ring. Qed. End NatPairsTimes. -Module NatPairsTimesProperties (NTimesModule : NTimesSignature). -Module Export NatPairsTimesModule := NatPairsTimes NTimesModule. +Module NatPairsTimesProperties (NTimesMod : NTimesSig). +Module Export NatPairsTimesModule := NatPairsTimes NTimesMod. Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule. End NatPairsTimesProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |