Commit 265a36d8 authored by Sergey Bozhko's avatar Sergey Bozhko

Shorten a proof

parent 1fba2ee2
Pipeline #31836 passed with stages
in 12 minutes and 11 seconds
......@@ -36,14 +36,13 @@ Section OffsetLemmas.
case: (boolP (j' == j)) => [/eqP EQ|NEQ]; first by rewrite -EQ.
specialize (PeanoNat.Nat.zero_or_succ (job_index arr_seq j')) => [Z_OR_SUCC].
move : Z_OR_SUCC => [Z | [m N]].
{ move: NEQ => /eqP NEQ; contradict NEQ.
apply (equal_index_implies_equal_jobs arr_seq) => //; first by rewrite TSK.
now rewrite Z INDX. }
{ have IND_LTE : (job_index arr_seq j <= job_index arr_seq j') by rewrite INDX N.
- move: NEQ => /eqP NEQ; contradict NEQ.
now eapply equal_index_implies_equal_jobs; eauto;
[rewrite TSK | rewrite Z INDX].
- have IND_LTE : (job_index arr_seq j <= job_index arr_seq j') by rewrite INDX N.
apply index_lte_implies_arrival_lte in IND_LTE => //; last by rewrite TSK.
move: H_valid_offset => [BEF_OFF AT_OFF].
move: (BEF_OFF j H_job_of_task) => BEF_OFF_j.
now ssromega. }
now apply/eqP; rewrite eqn_leq; apply/andP; split;
[ssromega | apply H_valid_offset].
Qed.
End OffsetLemmas.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment