proposition: Lemma path_to_S_standard_pathS : forall i j alpha beta, (i <= j)%nat -> path_toS beta (interval i j) alpha -> standard_pathS i alpha j beta.
proof: Proof. intros i j alpha beta H H0; unfold interval in H0. replace (S j - i)%nat with (S (j - i)) in H0 by lia. apply path_to_S_iota_from in H0. replace (j - i + i)%nat with j in H0 by lia. assumption. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)