Add basic lemmas to exploit hypotheses in behavior

This ensures all hypotheses in behavior have corresponding trivial lemmas in analysis/facts/all that enable to exploit them. This also makes the code more robust to potential changes in the precise way these hypotheses are stated.

analysis/facts/behavior/arrivals.v

@@ -109,7 +109,7 @@ Section Arrived.
       jobs_come_from_arrival_sequence sched arr_seq.
   Proof. by move=> ? []. Qed.
 
-  (** ... third, on the readiness of jobs in valid scheduleds. *)
+  (** ... third, on the readiness of jobs in valid schedules. *)
   Lemma valid_schedule_jobs_must_be_ready_to_execute :
     forall arr_seq,
       valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched.