proposition: Lemma path_toS_zero_but_last : forall x u alpha, path_toS zero (x::u) alpha -> u <> nil -> path_toS one (but_last x u) alpha.
proof: Proof. destruct u. - simpl; inversion 1. + now destruct 1. + now destruct 1. - intros alpha H H0; rewrite <- but_last_app in H. specialize (path_toS_appR H). intro H1; specialize (H1 (but_last x (n::u)) (simple_last x (n::u)::nil)). simpl in H1; destruct H1; try discriminate; auto. destruct H1. inversion H2. + destruct H4. symmetry in H6; destruct (canonS_zero_inv _ _ H6). * contradiction. * subst x0; simpl. subst alpha0; auto. + inversion H7. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)