diff options
Diffstat (limited to 'theories/Init/Peano.v')
| -rwxr-xr-x | theories/Init/Peano.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 2356c9cb59..d521a845d5 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -119,12 +119,24 @@ Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult). V8Infix "*" mult : nat_scope. +Lemma mult_O_r : (n:nat) (mult n O)=O. +Proof. + NewInduction n; Simpl; Auto. +Qed. + Lemma mult_n_O : (n:nat) O=(mult n O). Proof. NewInduction n; Simpl; Auto. Qed. Hints Resolve mult_n_O : core v62. +Lemma mult_S_r : (n,m:nat) (mult n (S m))=(plus (mult n m) n). +Proof. + Intros; NewInduction n as [|p H]; Simpl; Auto. + Rewrite H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S). + Pattern 1 3 m; Elim m; Simpl; Auto. +Qed. + Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)). Proof. Intros; NewInduction n as [|p H]; Simpl; Auto. |