diff --git a/HoareLogic.v b/HoareLogic.v
index d01b0ed..971b8bd 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -6,6 +6,8 @@
 Require Import Frap.
 
 
+
+
 (** * Syntax and semantics of a simple imperative language *)
 
 (* Here's some appropriate syntax for expressions (side-effect-free) of a simple
@@ -188,7 +190,7 @@ Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
 
 Infix "+" := plus : reset_scope.
-Infix "-" := minus : reset_scope.
+Infix "-" := Init.Nat.sub : reset_scope.
 Infix "*" := mult : reset_scope.
 Infix "=" := eq : reset_scope.
 Infix "<" := lt : reset_scope.
diff --git a/HoareLogic_template.v b/HoareLogic_template.v
index cfc9eff..67ff954 100644
--- a/HoareLogic_template.v
+++ b/HoareLogic_template.v
@@ -164,7 +164,7 @@ Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
 
 Infix "+" := plus : reset_scope.
-Infix "-" := minus : reset_scope.
+Infix "-" := Init.Nat.sub : reset_scope.
 Infix "*" := mult : reset_scope.
 Infix "=" := eq : reset_scope.
 Infix "<" := lt : reset_scope.