proposition: Lemma standard_pathS_path_toS : forall i alpha j beta, standard_pathS i alpha j beta -> (i <= j)%nat -> path_toS beta (interval i j) alpha.
proof: Proof. induction 1. - subst; rewrite interval_singleton. left; split; auto. - intros; rewrite interval_unroll. + eright; auto. * split; auto. intro;subst; cbn in H; apply standard_path_toS_zero in H; now destruct H. * apply IHstandard_path_toS; eapply standard_path_toS_le_inv; eauto. + eapply standard_path_toS_le_inv;eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)