proposition: Lemma standard_path_equiv_1 : forall i j alpha beta, standard_path i alpha j beta -> beta = standard_gnaw i alpha (S j - i)%nat.
proof: Proof. induction 1. - subst j; replace (S i - i)%nat with 1. + subst; reflexivity. + abstract lia. - subst beta; assert (i < j)%nat. { eapply standard_path_LE; apply H. } assert (H1 : (S j - i = S ( j - i))%nat) by lia. rewrite H1; simpl (standard_gnaw i alpha (S (S i - S j))); replace (S j - S i)%nat with (j - i)%nat; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)