proposition: Lemma trace_to_std i h j h': (i <= j)%nat -> trace_to h' (interval i j) h -> rounds standard i h (S j) h'.
proof: Proof. unfold interval. intro H. simpl in H. replace (S j - i)%nat with (S (j - i))%nat by lia. intro. apply trace_to_std_0 in H0. replace (S (j - i) + i)%nat with (S j) in H0 by lia. auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )