diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index 44539d945ebb06a24debeff8388f9bc0e46bd884..9c01810c7fe34e247a1cbed69b0974b117cecf6e 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -250,7 +250,6 @@ Section RelationToScheduled.
     rewrite /service_at /scheduled_at.
     move=> t NOT_SCHED.
     rewrite service_implies_scheduled //.
-      by apply: negbTE.
   Qed.
 
   (* Conversely, if a job receives service, then it must be scheduled. *)
@@ -354,8 +353,7 @@ Section RelationToScheduled.
     Proof.
       move=> t. rewrite /scheduled_at /service_at.
       split => [NOT_SCHED | NO_SERVICE].
-      - apply negbTE in NOT_SCHED.
-        by rewrite service_implies_scheduled //.
+      - by rewrite service_implies_scheduled //.
       - apply (contra (H_scheduled_implies_serviced j (sched t))).
         by rewrite -eqn0Ngt; apply /eqP => //.
     Qed.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index d52e29116bbe664259241b92a5b2c6e56c85d29a..a80b3b6976dcc763f2ec1148b686fcd3c838a233 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -9,16 +9,15 @@ Class ProcessorState (Job : JobType) (State : Type) :=
   {
     (* For a given processor state, the [scheduled_in] predicate checks whether a given
        job is running in that state. *)
-    scheduled_in: Job -> State -> bool;
+    scheduled_in : Job -> State -> bool;
     (* For a given processor state, the [service_in] function determines how much
        service a given job receives in that state. *)
-    service_in: Job -> State -> work;
+    service_in : Job -> State -> work;
     (* For a given processor state, a job does not receive service if it is not scheduled
        in that state *)
     service_implies_scheduled :
-      forall j s, scheduled_in j s = false -> service_in j s = 0
+      forall j s, ~~ scheduled_in j s -> service_in j s = 0
   }.
 
 (* A schedule maps an instant to a processor state *)
 Definition schedule (PState : Type) := instant -> PState.
-
diff --git a/restructuring/model/processor/ideal.v b/restructuring/model/processor/ideal.v
index ca65de81f8f96ca5258e1aebe13e6f8165da1e25..e692211e0187883fa8b894236fdd09fef2c13826 100644
--- a/restructuring/model/processor/ideal.v
+++ b/restructuring/model/processor/ideal.v
@@ -15,6 +15,6 @@ Section State.
       service_in j s   := s == Some j;
     }.
   Next Obligation.
-    by rewrite H.
+    by move: H=> /negbTE->.
   Defined.
 End State.
diff --git a/restructuring/model/processor/spin.v b/restructuring/model/processor/spin.v
index 44826d232cc7b76c011be60b4a29ea2b9b287785..931dc457fe0fb490f5097fcd1d1c7fbda44710e6 100644
--- a/restructuring/model/processor/spin.v
+++ b/restructuring/model/processor/spin.v
@@ -37,6 +37,7 @@ Section State.
       service_in   := service_in
     }.
   Next Obligation.
-    by move: H; case s => //= j' ->.
+    move: H.
+    by case: s=>//= j' /negbTE->.
   Defined.
 End State.
diff --git a/restructuring/model/processor/varspeed.v b/restructuring/model/processor/varspeed.v
index 2708b14902cccde2626a89f4ac96dcc001be31b0..a0dccb4b74025937ec106d9824cecdfbc18b3d92 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/restructuring/model/processor/varspeed.v
@@ -34,7 +34,7 @@ Section State.
     }.
   Next Obligation.
       move: j s H.
-      by move=> j []//= j' s->.
+      by move=> j []//= j' s/negbTE->.
   Defined.
-  
+
 End State.