proposition: Lemma standard_pathS_app i alpha j beta k gamma : (i <= j)%nat -> (j <= k)%nat -> standard_pathS i alpha j beta -> standard_pathS (S j) beta k gamma -> standard_pathS i alpha k gamma.
proof: Proof. intros; apply standard_pathS_path_toS in H1; auto. + apply standard_pathS_path_toS in H2. * generalize (path_toS_app H2 H1); intro H3; rewrite <- interval_app in H3; auto. unfold interval in H3; replace k with (( k - i) + i)%nat. apply path_to_S_iota_from; auto. -- replace (S (k - i))%nat with (S k - i)%nat; [auto | lia]. -- abstract lia. * eapply standard_path_toS_le_inv;eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)