diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NMinus.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMinus.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index 5ac1f70fb..fe0ec4e62 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -41,7 +41,7 @@ Qed. Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0. Proof. intros n m H; elim H using lt_ind_rel; clear n m H. -solve_rel_wd. +solve_relation_wd. intro; rewrite minus_0_r; apply neq_succ_0. intros; now rewrite minus_succ. Qed. |