proposition: Lemma path_to_standard_equiv i j alpha beta : i <> 0 -> (i <= j)%nat -> path_to beta (interval i j) alpha <-> standard_path i alpha j beta.
proof: Proof. intros H H0; destruct i, j. - now destruct H. - now destruct H. - inversion H0. - split; intro. + apply standard_path_shift. rewrite <- path_toS_standardS_equiv. * rewrite <- shift_interval in H1. now rewrite path_toS_path_to. * abstract lia. + rewrite <- shift_interval, <- path_toS_path_to; apply standard_path_unshift in H1. rewrite path_toS_standardS_equiv; auto. abstract lia. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)