proposition: Lemma standard_path_path_to i alpha j beta : standard_path i alpha j beta -> i <> 0 -> (i <= j)%nat -> path_to beta (interval i j) alpha.
proof: Proof. induction 1. - subst; rewrite interval_singleton. left; auto; red; destruct i. + now destruct H0. + split; auto. - intros; rewrite interval_unroll. + destruct i. * now destruct H0. * eright; auto. -- esplit. ++ intro; subst; simpl in H. apply standard_path_origin in H. now destruct H. ++ reflexivity. -- eapply IHstandard_path_to; eauto. eapply standard_path_to_le_inv;eauto. + eapply standard_path_to_le_inv;eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)