diff options
Diffstat (limited to 'theories/Init/Peano.v')
| -rw-r--r-- | theories/Init/Peano.v | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 8c6fba508..3c0fc02e4 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -30,9 +30,10 @@ Require Import Logic. Open Scope nat_scope. Definition eq_S := f_equal S. +Definition f_equal_nat := f_equal (A:=nat). -Hint Resolve (f_equal S): v62. -Hint Resolve (f_equal (A:=nat)): core. +Hint Resolve eq_S: v62. +Hint Resolve f_equal_nat: core. (** The predecessor function *) @@ -40,7 +41,8 @@ Definition pred (n:nat) : nat := match n with | O => n | S u => u end. -Hint Resolve (f_equal pred): v62. +Definition f_equal_pred := f_equal pred. +Hint Resolve f_equal_pred: v62. Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. @@ -88,8 +90,10 @@ Fixpoint plus (n m:nat) : nat := where "n + m" := (plus n m) : nat_scope. -Hint Resolve (f_equal2 plus): v62. -Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. +Definition f_equal2_plus := f_equal2 plus. +Hint Resolve f_equal2_plus: v62. +Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). +Hint Resolve f_equal2_nat: core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. @@ -127,8 +131,8 @@ Fixpoint mult (n m:nat) : nat := end where "n * m" := (mult n m) : nat_scope. - -Hint Resolve (f_equal2 mult): core. +Definition f_equal2_mult := f_equal2 mult. +Hint Resolve f_equal2_mult: core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. |