proposition: Lemma gnaw_to_path_to : forall s alpha beta, beta = gnaw alpha s -> ~ In 0 s -> beta <> zero -> s <> nil -> path_to beta s alpha.
proof: Proof. intros; rewrite path_to_path_toS_iff; auto. apply gnawS_to_path_toS; auto. - now rewrite gnaw_gnawS in H; auto. - destruct s. + now destruct H2. + destruct n. * destruct H0; now left. * discriminate. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)