diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala
index afb8d01..28ec9b5 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala
@@ -8,6 +8,9 @@ import scala.language.postfixOps
   */
 object GenerativeFluentAssertionsDSL:
 
+  extension (inline property: AssertionProperty)
+    inline def `unary_!`: AssertionProperty = NegatedAssertionProperty(property)
+
   /**
    * Due to operator precedence, '!==' is the only comparison operator that is considered an "assignment operation"
    * and thus has lower precedence than alphanumeric operators. Therefore, we must handle "!==" as the final link of
@@ -39,6 +42,19 @@ object GenerativeFluentAssertionsDSL:
     assertionsGenerativeImpl('assertions)
   }
 
+  private def unwrapShouldBeNegatedAssertion(assertionExpr: Expr[AssertionProperty], negated: Boolean = false)(
+    using Quotes
+  ): (Expr[String], Boolean) =
+    import quotes.reflect.*
+
+    assertionExpr match
+      case '{ NegatedAssertionProperty($innerExpr: AssertionProperty) } => unwrapShouldBeNegatedAssertion(innerExpr, !negated)
+      case '{ be.selectDynamic($propertyNameExpr: String) } => (propertyNameExpr, negated)
+      case what => report.errorAndAbort(
+        "'be' negation unwrapping: Invalid expression, must be a 'should be' assertion.",
+        what
+      )
+
   /** Macro implementation. The method is recursive, each single expression is
     * then separately rewritten into the generateAssertion method. The method
     * returns a compiler error if the expression is not an AssertionProperty.
@@ -84,12 +100,9 @@ object GenerativeFluentAssertionsDSL:
 
     val generatedAssertion = assertionExpr match
       // be assertion. Check the explicit selectDynamic to extract the property name
-      case '{
-            (${ subjectExpr }: subjectType) should be.selectDynamic(
-              $propertyNameExpr
-            )
-          } =>
-        generateShouldBeAssertion[subjectType](subjectExpr, propertyNameExpr)
+      case '{ (${ subjectExpr }: subjectType) should ($assertionProperty: AssertionProperty) } =>
+        val (propertyNameExpr, negated) = unwrapShouldBeNegatedAssertion(assertionProperty)
+        generateShouldBeAssertion[subjectType](subjectExpr, propertyNameExpr, negated)
       // The more complicated structure of property type provider construction in
       // the should have assertion. Again, the applyDynamic is explicit.
       // The quoted pattern also extracts: the type of the assertion subject,
@@ -101,10 +114,12 @@ object GenerativeFluentAssertionsDSL:
           } =>
         println(assertionExpr.show)
         val subjectExpr = '{ $typeProvider.subject }
+        val negatedExpr = '{ $typeProvider.negated }
         generateShouldHaveAssertion[subjectType, valueType](
           subjectExpr,
           propertyNameExpr,
-          valueExpr
+          valueExpr,
+          negatedExpr
         )
       case '{
             (${ typeProvider }: BePropertyTypeProvider[subjectType])
@@ -119,7 +134,6 @@ object GenerativeFluentAssertionsDSL:
       } =>
         '{} // placeholder
       case _ =>
-        println(assertionExpr.show)
         report.errorAndAbort(
           "Invalid expression, must be a 'should be' or 'should have' assertion. ",
           assertionExpr
@@ -130,7 +144,8 @@ object GenerativeFluentAssertionsDSL:
 
   private def generateShouldBeAssertion[T](
       subject: Expr[T],
-      propertyNameExpr: Expr[String]
+      propertyNameExpr: Expr[String],
+      negated: Boolean
   )(using Type[T])(using Quotes): Expr[Unit] =
     import quotes.reflect.*
 
@@ -153,11 +168,12 @@ object GenerativeFluentAssertionsDSL:
       // Constructs a 'select' tree, that is, a selection to the field or method
       // of the subject.
       val call = Select(subject.asTerm, validSymbol).asExprOf[Boolean]
+      val expected = '{ !${Expr(negated)} }
 
       val assertion = '{
         assert(
-          $call,
-          s"${$subject} was not ${$propertyNameExpr} (${$validSymbolNameExpr} is false)"
+          $call == $expected,
+          s"${$subject} was${if ($expected) " not" else ""} ${$propertyNameExpr} (${$validSymbolNameExpr} is ${if ($expected) "false" else "true"})"
         )
       }
       assertion
@@ -167,7 +183,8 @@ object GenerativeFluentAssertionsDSL:
   private def generateShouldHaveAssertion[T, R](
       subjectExpr: Expr[T],
       propertyNameExpr: Expr[String],
-      propertyValueExpr: Expr[Condition[R]]
+      propertyValueExpr: Expr[Condition[R]],
+      negatedExpr: Expr[Boolean]
   )(using Type[T], Type[R])(using Quotes): Expr[Unit] =
     import quotes.reflect.*
 
@@ -200,11 +217,13 @@ object GenerativeFluentAssertionsDSL:
        */
       val assertion = '{
         val subject = $subjectExpr
+        val negated = $negatedExpr
         val condition = $propertyValueExpr
         lazy val value = ${ Select(('subject).asTerm, candidateMethod).asExprOf[R] }
+
         assert(
-          condition.test(value),
-          s"${subject}.${$propertyNameExpr} " + condition.failedMessage + " but " + value
+          condition.test(value) == !negated,
+          s"${subject}.${$propertyNameExpr} " + condition.failedMessage(negated) + " but " + value
         )
       }
       report.info(assertion.show, subjectExpr.asTerm.pos)
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala
index bb3902c..0370895 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala
@@ -3,6 +3,7 @@ package ch.usi.si.msde.edsl.lecture10
 import scala.language.dynamics
 
 sealed trait AssertionProperty
+case class NegatedAssertionProperty(prop: AssertionProperty) extends AssertionProperty
 
 /** Represents (but with no implementation) the result of a call to
   * be.selectDynamic(String), used to specify the property. The semantics of
@@ -19,35 +20,24 @@ end DynamicShouldBeProperty
  */
 sealed trait SatisfyingNotEquals[T]
 
-case class Condition[T](predicate: (T, T) => Boolean, op: String, expected: T):
-  def test(value: T): Boolean = predicate(value, expected)
-  def failedMessage: String = s"is not ${op} ${expected}"
+case class Condition[-T](predicate: T => Boolean, op: String, expected: Any):
+  def test(value: T): Boolean = predicate(value)
+  def failedMessage(negated: Boolean): String = s"${if (negated) "is" else "is not"} ${op} ${expected}"
 
 case object satisfying:
-  def `===`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.equiv, "===", toWhat)
-  def notEquals[T](toWhat: T, ord: Ordering[T]): Condition[T] = Condition(!ord.equiv(_, _), "!==", toWhat)
-  def `<`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.lt, "<", toWhat)
-  def `>`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.gt, ">", toWhat)
-  def `<=`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.lteq, "<=", toWhat)
-  def `>=`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.gteq, ">=", toWhat)
+  def `===`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.equiv(_, toWhat), "===", toWhat)
+  def notEquals[T](toWhat: T, ord: Ordering[T]): Condition[T] = Condition(!ord.equiv(_, toWhat), "!==", toWhat)
+  def `<`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.lt(_, toWhat), "<", toWhat)
+  def `>`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.gt(_, toWhat), ">", toWhat)
+  def `<=`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.lteq(_, toWhat), "<=", toWhat)
+  def `>=`[T](toWhat: T)(using ord: Ordering[T]): Condition[T] = Condition(ord.gteq(_, toWhat), ">=", toWhat)
 
 class BePropertyTypeProvider[T](val subject: T) extends Selectable:
   def selectDynamic(fieldName: String): AssertionProperty = ???
   def applyDynamic(fieldName: String)(foo: Any*): AssertionProperty = ???
 end BePropertyTypeProvider
 
-/** The class that implements the syntactic aspect of the type provider. It
-  * extends Selectable and implements applyDynamic with arity 1, so that any
-  * object of this type can be invoked with an arbitrary method with 1 argument,
-  * and a specific return type.
-  *
-  * Selectable types can be refined with a list of specific methods that are
-  * available and thus checked by the compiler. The macro in the should method
-  * generates a refinement of this type according to type T, so that - for any
-  * arity zero method or field in T - say foo: X, the type provider has a
-  * corresponding method def foo(arg: X): AssertionProperty.
-  */
-class HavePropertyTypeProvider[T](val subject: T) extends Selectable:
+class HavePropertyTypeProvider[T](val subject: T, val negated: Boolean) extends Selectable:
   def applyDynamic[U](fieldName: String)(arg: satisfying.type): SatisfyingNotEquals[U] = ???
   def applyDynamic(fieldName: String)(arg: Any): AssertionProperty = ???
 end HavePropertyTypeProvider
@@ -58,7 +48,11 @@ sealed trait AssertionDSLVerb
 case object be extends AssertionDSLVerb with Dynamic:
   def selectDynamic(fieldName: String): AssertionProperty = ???
 case object be_ extends AssertionDSLVerb
-case object have extends AssertionDSLVerb
+
+sealed trait HaveVerb(val negated: Boolean):
+  inline def `unary_!`: HaveVerb = HaveNegation(this)
+case class HaveNegation(haveVerb: HaveVerb) extends HaveVerb(!haveVerb.negated)
+case object have extends HaveVerb(false)
 
 /** Implicit class to add 'should' assertions to a generic type T.
   *
@@ -90,11 +84,11 @@ extension [T](subject: T)
     *
     * The method semantics is then provided by the assertions macro.
     *
-    * @param verbWord
+    * @param verb
     *   The have word.
     * @return
     *   a type provider for properties of type T.
     */
-  transparent inline def should(inline verbWord: have.type) = ${
-    ShouldHaveTypeProvider.generateShouldHaveTypeProvider[T]('subject)
+  transparent inline def should(inline verb: HaveVerb) = ${
+    ShouldHaveTypeProvider.generateShouldHaveTypeProvider[T]('subject, '{verb.negated})
   }
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala
index 1293ddc..306ebf0 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala
@@ -26,7 +26,7 @@ case class Box(label: String, weight: Mass, price: Money)
   assertions:
     /* be.property assertions */
     // assert(person.adult, ...)
-    person should be.adult
+    person should !be.adult
     // assert(List().isEmpty, ...)
     List() should be.empty
     // assert(List(1,2,3).nonEmpty)
@@ -45,7 +45,7 @@ case class Box(label: String, weight: Mass, price: Money)
     List() should have size satisfying >= 0
     List(3) should have size satisfying !== 0
     List(50, 2, 3) should have head satisfying < 100
-    box should have weight satisfying <= 300.0.kg
+    box should !(!have) weight satisfying <= 300.0.kg
 
 /* should have assertions */
 //    // assert(List(1).head == 1, ...)
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala
index 179e244..5ebaeb3 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala
@@ -7,7 +7,7 @@ object ShouldHaveTypeProvider:
   /** The type provider for the should have assertion, which generates a refined
     * structural type for type T.
     */
-  def generateShouldHaveTypeProvider[T](subject: Expr[T])(using Type[T])(using
+  def generateShouldHaveTypeProvider[T](subject: Expr[T], negated: Expr[Boolean])(using Type[T])(using
       Quotes
   ): Expr[Any] =
     import quotes.reflect.*
@@ -86,10 +86,6 @@ object ShouldHaveTypeProvider:
     // exact type is unknown until compilation time.
     refinedType.asType match
       case '[tpe] => // tpe is the exact refined type
-        val res = '{
-          val p = HavePropertyTypeProvider[T]($subject)
-          p.asInstanceOf[tpe]
-        }
-        res
+        '{ HavePropertyTypeProvider[T]($subject, $negated).asInstanceOf[tpe] }
 
 end ShouldHaveTypeProvider