add lemma relating task cost and task rbf

Currently, we have lemmas stating that task_rbf at \vareosilon is greater than equal to task cost, and task_rbf is monotone. I combined these two lemmas to state that tsk_rbf at any point greater than 0 is greater than task cost. I find that this fact is regularly required in proofs and therefore, would be good to have in the facts folder.

analysis/facts/model/rbf.v

@@ -272,7 +272,7 @@ Section RequestBoundFunctions.
   Hypothesis H_j_arrives : arrives_in arr_seq j.
   Hypothesis H_job_of_tsk : job_of_task tsk j.
 
-  (** Then we prove that [task_rbf] at [ε] is greater than or equal to task cost. *)
+  (** Then we prove that [task_rbf] at [ε] is greater than or equal to the task's WCET. *)
   Lemma task_rbf_1_ge_task_cost:
     task_rbf ε >= task_cost tsk.
   Proof.
@@ -296,6 +296,18 @@ Section RequestBoundFunctions.
     by rewrite CONS.
   Qed.
 
+  (** As a corollary, we prove that the [task_rbf] at any point [A] greater than
+      [0] is no less than the task's WCET. *)
+  Lemma task_rbf_ge_task_cost:
+    forall A,
+      A > 0 ->
+      task_rbf A >= task_cost tsk.
+  Proof.
+    case => // A GEQ.
+    apply: (leq_trans task_rbf_1_ge_task_cost).
+    exact: task_rbf_monotone.
+  Qed.
+
   (** Assume that [tsk] has a positive cost. *)
   Hypothesis H_positive_cost : 0 < task_cost tsk.