proposition: Lemma path_toS_standardS_equiv i j alpha beta : (i <= j)%nat -> path_toS beta (interval i j) alpha <-> standard_pathS i alpha j beta.
proof: Proof. split; intros H0. - now apply path_to_S_standard_pathS. - now apply standard_pathS_path_toS. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)