Library prosa.analysis.facts.tdma


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


Require Export prosa.model.schedule.tdma.
Require Import prosa.util.all.
From mathcomp Require Import div.

In this section, we define the properties of TDMA and prove some basic lemmas.
Section TDMAFacts.
  Context {Task:eqType}.

Consider any task set ts...
  Variable ts: {set Task}.

... with a TDMA policy
  Context `{TDMAPolicy Task}.

  Section TimeSlotFacts.
Consider any task in ts
    Variable task: Task.
    Hypothesis H_task_in_ts: task \in ts.

Assume task_time_slot is valid time slot
    Hypothesis time_slot_positive:
      valid_time_slot ts.

Obviously, the TDMA cycle is greater or equal than any task time slot which is in TDMA cycle
    Lemma TDMA_cycle_ge_each_time_slot:
      TDMA_cycle ts task_time_slot task.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 29)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  task_time_slot task <= TDMA_cycle ts

----------------------------------------------------------------------------- *)


    Proof.
      rewrite /TDMA_cycle (big_rem task) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 47)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  task_time_slot task <=
  addn_comoid (task_time_slot task)
    (\big[addn_comoid/0]_(y <- rem (T:=Task) task ts) task_time_slot y)

----------------------------------------------------------------------------- *)


      apply:leq_trans; last by exact: leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 93)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  task_time_slot task <= task_time_slot task

----------------------------------------------------------------------------- *)


        by apply leqnn.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

Thus, a TDMA cycle is always positive
    Lemma TDMA_cycle_positive:
      TDMA_cycle ts > 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 32)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  0 < TDMA_cycle ts

----------------------------------------------------------------------------- *)


    Proof.
      move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

Slot offset is less then cycle
    Lemma Offset_lt_cycle:
      task_slot_offset ts task < TDMA_cycle ts.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 37)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  task_slot_offset ts task < TDMA_cycle ts

----------------------------------------------------------------------------- *)


    Proof.
      rewrite /task_slot_offset /TDMA_cycle big_mkcond.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \big[addn_monoid/0]_(i <- ts)
     (if slot_order i task && (i != task) then task_time_slot i else 0) <
  \sum_(tsk <- ts) task_time_slot tsk

----------------------------------------------------------------------------- *)


      apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 62)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \big[addn_monoid/0]_(i <- ts)
     (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  \sum_(prev_task <- ts)
     (if prev_task != task then task_time_slot prev_task else 0)

subgoal 2 (ID 63) is:
 \sum_(prev_task <- ts)
    (if prev_task != task then task_time_slot prev_task else 0) <
 \sum_(tsk <- ts) task_time_slot tsk

----------------------------------------------------------------------------- *)


      - apply leq_sum.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 64)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  forall i : Task,
  true ->
  (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  (if i != task then task_time_slot i else 0)

subgoal 2 (ID 63) is:
 \sum_(prev_task <- ts)
    (if prev_task != task then task_time_slot prev_task else 0) <
 \sum_(tsk <- ts) task_time_slot tsk

----------------------------------------------------------------------------- *)


intros× T.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 66)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  i : Task
  T : true
  ============================
  (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  (if i != task then task_time_slot i else 0)

subgoal 2 (ID 63) is:
 \sum_(prev_task <- ts)
    (if prev_task != task then task_time_slot prev_task else 0) <
 \sum_(tsk <- ts) task_time_slot tsk

----------------------------------------------------------------------------- *)


case (slot_order i task);auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 63)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \sum_(prev_task <- ts)
     (if prev_task != task then task_time_slot prev_task else 0) <
  \sum_(tsk <- ts) task_time_slot tsk

----------------------------------------------------------------------------- *)


      - rewrite -big_mkcond (bigD1_seq task)?set_uniq//=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \sum_(i <- ts | i != task) task_time_slot i <
  task_time_slot task + \sum_(i <- ts | i != task) task_time_slot i

----------------------------------------------------------------------------- *)


        rewrite -subn_gt0 -addnBA.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 143)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  0 <
  task_time_slot task +
  (\sum_(i <- ts | i != task) task_time_slot i -
   \sum_(i <- ts | i != task) task_time_slot i)

subgoal 2 (ID 144) is:
 \sum_(i <- ts | i != task) task_time_slot i <=
 \sum_(i <- ts | i != task) task_time_slot i

----------------------------------------------------------------------------- *)


rewrite subnn addn0 //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 154)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  0 < task_time_slot task

subgoal 2 (ID 144) is:
 \sum_(i <- ts | i != task) task_time_slot i <=
 \sum_(i <- ts | i != task) task_time_slot i

----------------------------------------------------------------------------- *)


        exact: time_slot_positive.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 144)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \sum_(i <- ts | i != task) task_time_slot i <=
  \sum_(i <- ts | i != task) task_time_slot i

----------------------------------------------------------------------------- *)


        easy.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

For a task, the sum of its slot offset and its time slot is less then or equal to cycle.
    Lemma Offset_add_slot_leq_cycle:
      task_slot_offset ts task + task_time_slot task TDMA_cycle ts.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  task_slot_offset ts task + task_time_slot task <= TDMA_cycle ts

----------------------------------------------------------------------------- *)


    Proof.
      rewrite /task_slot_offset /TDMA_cycle.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
     task_time_slot prev_task + task_time_slot task <=
  \sum_(tsk <- ts) task_time_slot tsk

----------------------------------------------------------------------------- *)


      rewrite addnC (bigD1_seq task) //=.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 74)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  task_time_slot task +
  \sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
     task_time_slot prev_task <=
  task_time_slot task + \sum_(i <- ts | i != task) task_time_slot i

subgoal 2 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


rewrite leq_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 123)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \sum_(prev_task <- ts | slot_order prev_task task && (prev_task != task))
     task_time_slot prev_task <= \sum_(i <- ts | i != task) task_time_slot i

subgoal 2 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


      rewrite big_mkcond.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 132)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \big[addn_monoid/0]_(i <- ts)
     (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  \sum_(i <- ts | i != task) task_time_slot i

subgoal 2 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


      replace (\sum_(i <- ts | i != task) task_time_slot i)
        with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 153)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \big[addn_monoid/0]_(i <- ts)
     (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  \sum_(i <- ts) (if i != task then task_time_slot i else 0)

subgoal 2 (ID 150) is:
 \sum_(i <- ts) (if i != task then task_time_slot i else 0) =
 \sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


      apply leq_sum.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 155)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  forall i : Task,
  true ->
  (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  (if i != task then task_time_slot i else 0)

subgoal 2 (ID 150) is:
 \sum_(i <- ts) (if i != task then task_time_slot i else 0) =
 \sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


intros×T.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 157)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  i : Task
  T : true
  ============================
  (if slot_order i task && (i != task) then task_time_slot i else 0) <=
  (if i != task then task_time_slot i else 0)

subgoal 2 (ID 150) is:
 \sum_(i <- ts) (if i != task then task_time_slot i else 0) =
 \sum_(i <- ts | i != task) task_time_slot i
subgoal 3 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


case (slot_order i task);auto.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 150)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  \sum_(i <- ts) (if i != task then task_time_slot i else 0) =
  \sum_(i <- ts | i != task) task_time_slot i

subgoal 2 (ID 97) is:
 uniq ts

----------------------------------------------------------------------------- *)


        by rewrite -big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  ============================
  uniq ts

----------------------------------------------------------------------------- *)


apply (set_uniq ts).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.
  End TimeSlotFacts.

Now we prove that no two tasks share the same time slot at any time.
  Section TimeSlotOrderFacts.
Consider any task in ts
    Variable task: Task.
    Hypothesis H_task_in_ts: task \in ts.

Assume task_time_slot is valid time slot
    Hypothesis time_slot_positive:
      valid_time_slot ts.

Assume that slot order is total...
    Hypothesis slot_order_total:
      total_slot_order ts.

    (*..., antisymmetric... *)
    Hypothesis slot_order_antisymmetric:
      antisymmetric_slot_order ts.

    (*... and transitive. *)
    Hypothesis slot_order_transitive:
      transitive_slot_order.

Then, we can prove that the difference value between two offsets is at least a slot
    Lemma relation_offset:
       tsk1 tsk2, tsk1 \in ts
                                 tsk2 \in ts
                                          slot_order tsk1 tsk2
                                          tsk1 != tsk2
                                          task_slot_offset ts tsk2
                                          task_slot_offset ts tsk1 + task_time_slot tsk1 .

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  ============================
  forall tsk1 tsk2 : Task,
  tsk1 \in ts ->
  tsk2 \in ts ->
  slot_order tsk1 tsk2 ->
  tsk1 != tsk2 ->
  task_slot_offset ts tsk1 + task_time_slot tsk1 <= task_slot_offset ts tsk2

----------------------------------------------------------------------------- *)


    Proof.
      intros× IN1 IN2 ORDER NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  task_slot_offset ts tsk1 + task_time_slot tsk1 <= task_slot_offset ts tsk2

----------------------------------------------------------------------------- *)


      rewrite /task_slot_offset big_mkcond addnC/=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  task_time_slot tsk1 +
  \sum_(i <- ts)
     (if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
  \sum_(prev_task <- ts | slot_order prev_task tsk2 && (prev_task != tsk2))
     task_time_slot prev_task

----------------------------------------------------------------------------- *)


      replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
        with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 105)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  task_time_slot tsk1 +
  \sum_(i <- ts)
     (if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


      rewrite leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 111)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  \sum_(i <- ts)
     (if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


apply leq_sum_seq.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 112)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  forall i : Task,
  i \in ts ->
  true ->
  (if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
  (if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
   then task_time_slot i
   else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


intros× IN T.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 115)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  i : Task
  IN : i \in ts
  T : true
  ============================
  (if slot_order i tsk1 && (i != tsk1) then task_time_slot i else 0) <=
  (if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
   then task_time_slot i
   else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


      case (slot_order i tsk1)eqn:SI2;auto.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 129)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  i : Task
  IN : i \in ts
  T : true
  SI2 : slot_order i tsk1 = true
  ============================
  (if true && (i != tsk1) then task_time_slot i else 0) <=
  (if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
   then task_time_slot i
   else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


case (i==tsk1)eqn:IT2;auto;simpl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 195)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  i : Task
  IN : i \in ts
  T : true
  SI2 : slot_order i tsk1 = true
  IT2 : (i == tsk1) = false
  ============================
  task_time_slot i <=
  (if slot_order i tsk2 && true && (i != tsk2) then task_time_slot i else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


      case (i==tsk2)eqn:IT1;simpl;auto.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 210)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  i : Task
  IN : i \in ts
  T : true
  SI2 : slot_order i tsk1 = true
  IT2 : (i == tsk1) = false
  IT1 : (i == tsk2) = true
  ============================
  task_time_slot i <=
  (if slot_order i tsk2 && true && false then task_time_slot i else 0)

subgoal 2 (ID 211) is:
 task_time_slot i <=
 (if slot_order i tsk2 && true && true then task_time_slot i else 0)
subgoal 3 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


      - by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 211)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  i : Task
  IN : i \in ts
  T : true
  SI2 : slot_order i tsk1 = true
  IT2 : (i == tsk1) = false
  IT1 : (i == tsk2) = false
  ============================
  task_time_slot i <=
  (if slot_order i tsk2 && true && true then task_time_slot i else 0)

subgoal 2 (ID 102) is:
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0) =
 \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


      - by rewrite (slot_order_transitive _ _ _ SI2 ORDER).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0) =
  \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk

----------------------------------------------------------------------------- *)


      - symmetry.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 488)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  \sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk =
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


rewrite big_mkcond /=.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 498)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  \sum_(i <- ts)
     (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) =
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


rewritebigD1_seq with (j:=tsk1);auto;last by apply (set_uniq ts).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 500)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2
  NEQ : tsk1 != tsk2
  ============================
  addn_comoid
    (if slot_order tsk1 tsk2 && (tsk1 != tsk2)
     then task_time_slot tsk1
     else 0)
    (\big[addn_comoid/0]_(i <- ts | i != tsk1)
        (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


        move/eqP /eqP in ORDER.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 622)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  NEQ : tsk1 != tsk2
  ORDER : slot_order tsk1 tsk2 = true
  ============================
  addn_comoid
    (if slot_order tsk1 tsk2 && (tsk1 != tsk2)
     then task_time_slot tsk1
     else 0)
    (\big[addn_comoid/0]_(i <- ts | i != tsk1)
        (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 686)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  ============================
  addn_comoid
    (if slot_order tsk1 tsk2 && (tsk1 != tsk2)
     then task_time_slot tsk1
     else 0)
    (\big[addn_comoid/0]_(i <- ts | i != tsk1)
        (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0)) =
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


rewrite ORDER //=.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 689)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  ============================
  (if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
  \sum_(i <- ts | i != tsk1)
     (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) =
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 766)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  ============================
  (if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
  \sum_(i <- ts | i != tsk1)
     (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


        have TS2: (tsk1 != tsk2) = true .
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 769)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  ============================
  (tsk1 != tsk2) = true

subgoal 2 (ID 771) is:
 (if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
 \sum_(i <- ts | i != tsk1)
    (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
 task_time_slot tsk1 +
 \sum_(tsk <- ts)
    (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
     then task_time_slot tsk
     else 0)

----------------------------------------------------------------------------- *)


apply /eqP;auto.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 771)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  ============================
  (if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
  \sum_(i <- ts | i != tsk1)
     (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


rewrite TS2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 811)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  ============================
  task_time_slot tsk1 +
  \sum_(i <- ts | i != tsk1)
     (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
  task_time_slot tsk1 +
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


        rewrite eqn_add2l.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 816)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  ============================
  \sum_(i <- ts | i != tsk1)
     (if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0) ==
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


rewrite big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 825)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  ============================
  \big[addn_monoid/0]_(i <- ts)
     (if i != tsk1
      then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
      else 0) ==
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 853)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  ============================
  \big[addn_monoid/0]_(i <- ts)
     (if i != tsk1
      then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
      else 0) =
  \sum_(tsk <- ts)
     (if slot_order tsk tsk2 && (tsk != tsk1) && (tsk != tsk2)
      then task_time_slot tsk
      else 0)

----------------------------------------------------------------------------- *)


apply eq_bigr;auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 854)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  ============================
  forall i : Task,
  true ->
  (if i != tsk1
   then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
   else 0) =
  (if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
   then task_time_slot i
   else 0)

----------------------------------------------------------------------------- *)


        intros× T.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 860)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  IN1 : tsk1 \in ts
  IN2 : tsk2 \in ts
  ORDER : slot_order tsk1 tsk2 = true
  NEQ : tsk1 <> tsk2
  TS2 : (tsk1 != tsk2) = true
  i : Task
  T : true
  ============================
  (if i != tsk1
   then if slot_order i tsk2 && (i != tsk2) then task_time_slot i else 0
   else 0) =
  (if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
   then task_time_slot i
   else 0)

----------------------------------------------------------------------------- *)


case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

Then, we proved that no two tasks share the same time slot at any time.
    Lemma task_in_time_slot_uniq:
       tsk1 tsk2 t, tsk1 \in ts task_time_slot tsk1 > 0
                                   tsk2 \in ts task_time_slot tsk2 > 0
                                            task_in_time_slot ts tsk1 t
                                            task_in_time_slot ts tsk2 t
                                            tsk1 = tsk2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 75)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  ============================
  forall (tsk1 tsk2 : Task) (t : instant),
  tsk1 \in ts ->
  0 < task_time_slot tsk1 ->
  tsk2 \in ts ->
  0 < task_time_slot tsk2 ->
  task_in_time_slot ts tsk1 t -> task_in_time_slot ts tsk2 t -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


    Proof.
      intros× IN1 SLOT1 IN2 SLOT2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 82)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  ============================
  task_in_time_slot ts tsk1 t -> task_in_time_slot ts tsk2 t -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      rewrite /task_in_time_slot.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  ============================
  (t + TDMA_cycle ts - task_slot_offset ts tsk1 %% TDMA_cycle ts)
  %% TDMA_cycle ts < task_time_slot tsk1 ->
  (t + TDMA_cycle ts - task_slot_offset ts tsk2 %% TDMA_cycle ts)
  %% TDMA_cycle ts < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      set cycle:=TDMA_cycle ts.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  ============================
  (t + cycle - task_slot_offset ts tsk1 %% cycle) %% cycle <
  task_time_slot tsk1 ->
  (t + cycle - task_slot_offset ts tsk2 %% cycle) %% cycle <
  task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      set O1:= task_slot_offset ts tsk1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  ============================
  (t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
  (t + cycle - task_slot_offset ts tsk2 %% cycle) %% cycle <
  task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      set O2:= task_slot_offset ts tsk2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  ============================
  (t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have CO1: O1 < cycle by apply Offset_lt_cycle.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  ============================
  (t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have CO2: O2 < cycle by apply Offset_lt_cycle.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 107)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  ============================
  (t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have C: cycle > 0 by apply (TDMA_cycle_positive tsk1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 112)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  ============================
  (t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 119)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  ============================
  (t + cycle - O1 %% cycle) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


rewrite GO1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  ============================
  (t + cycle - O1) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  ============================
  (t + cycle - O1) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2 %% cycle) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


rewrite GO2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 130)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  ============================
  (t + cycle - O1) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have SO1:O1 + task_time_slot tsk1 cycle by apply (Offset_add_slot_leq_cycle tsk1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 136)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  ============================
  (t + cycle - O1) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      have SO2:O2 + task_time_slot tsk2 cycle by apply (Offset_add_slot_leq_cycle tsk2).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 142)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  ============================
  (t + cycle - O1) %% cycle < task_time_slot tsk1 ->
  (t + cycle - O2) %% cycle < task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      repeat rewrite mod_elim;auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 158)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  ============================
  (if O1 <= t %% cycle then t %% cycle - O1 else t %% cycle + cycle - O1) <
  task_time_slot tsk1 ->
  (if O2 <= t %% cycle then t %% cycle - O2 else t %% cycle + cycle - O2) <
  task_time_slot tsk2 -> tsk1 = tsk2

----------------------------------------------------------------------------- *)


      case (O1 t%%cycle)eqn:O1T;case (O2 t %%cycle)eqn:O2T;intros G1 G2;try ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 238)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  O1T : (O1 <= t %% cycle) = true
  O2T : (O2 <= t %% cycle) = true
  G1 : t %% cycle - O1 < task_time_slot tsk1
  G2 : t %% cycle - O2 < task_time_slot tsk2
  ============================
  tsk1 = tsk2

----------------------------------------------------------------------------- *)


      apply ltn_subLR in G1;apply ltn_subLR in G2.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2943)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  O1T : (O1 <= t %% cycle) = true
  O2T : (O2 <= t %% cycle) = true
  G1 : t %% cycle < task_time_slot tsk1 + O1
  G2 : t %% cycle < task_time_slot tsk2 + O2
  ============================
  tsk1 = tsk2

----------------------------------------------------------------------------- *)


case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 3097)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  O1T : (O1 <= t %% cycle) = true
  O2T : (O2 <= t %% cycle) = true
  G1 : t %% cycle < task_time_slot tsk1 + O1
  G2 : t %% cycle < task_time_slot tsk2 + O2
  NEQ : tsk1 <> tsk2
  ============================
  tsk1 = tsk2

----------------------------------------------------------------------------- *)


      destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
      fold O1 O2 in order;try ssrlia;auto.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3171)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  O1T : (O1 <= t %% cycle) = true
  O2T : (O2 <= t %% cycle) = true
  G1 : t %% cycle < task_time_slot tsk1 + O1
  G2 : t %% cycle < task_time_slot tsk2 + O2
  NEQ : tsk1 <> tsk2
  order : slot_order tsk1 tsk2
  ============================
  tsk1 != tsk2

subgoal 2 (ID 3175) is:
 tsk2 != tsk1

----------------------------------------------------------------------------- *)


by move/eqP in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 3175)
  
  Task : eqType
  ts : {setTask}
  H : TDMAPolicy Task
  task : Task
  H_task_in_ts : task \in ts
  time_slot_positive : valid_time_slot ts
  slot_order_total : total_slot_order ts
  slot_order_antisymmetric : antisymmetric_slot_order ts
  slot_order_transitive : transitive_slot_order
  tsk1, tsk2 : Task
  t : instant
  IN1 : tsk1 \in ts
  SLOT1 : 0 < task_time_slot tsk1
  IN2 : tsk2 \in ts
  SLOT2 : 0 < task_time_slot tsk2
  cycle := TDMA_cycle ts : nat
  O1 := task_slot_offset ts tsk1 : nat
  O2 := task_slot_offset ts tsk2 : nat
  CO1 : O1 < cycle
  CO2 : O2 < cycle
  C : 0 < cycle
  GO1 : O1 %% cycle = O1
  GO2 : O2 %% cycle = O2
  SO1 : O1 + task_time_slot tsk1 <= cycle
  SO2 : O2 + task_time_slot tsk2 <= cycle
  O1T : (O1 <= t %% cycle) = true
  O2T : (O2 <= t %% cycle) = true
  G1 : t %% cycle < task_time_slot tsk1 + O1
  G2 : t %% cycle < task_time_slot tsk2 + O2
  NEQ : tsk1 <> tsk2
  order : slot_order tsk2 tsk1
  ============================
  tsk2 != tsk1

----------------------------------------------------------------------------- *)


apply /eqP;auto.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End TimeSlotOrderFacts.
End TDMAFacts.