proposition: Lemma standard_path_equiv_2 : forall l i alpha, i <> 0 -> let beta := standard_gnaw i alpha (S l) in beta <> zero -> standard_path i alpha (l + i)%nat beta.
proof: Proof. induction l as [| l IHl]. - cbn; left; auto. intro; subst alpha; now destruct i, H0. - right; specialize (IHl (S i) (canon alpha i)); simpl standard_gnaw in *. replace ((S l) +i )%nat with (l + S i)%nat. + apply IHl; auto. + abstract lia. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)