proposition: Lemma mlargeS_iff alpha x s : s <>nil -> mlargeS alpha (x::s) <-> gnawS alpha (but_last x s) = one.
proof: Proof. intro H; split. - intros H0; generalize (path_toS_zero_but_last H0 H); intro H1; apply path_toS_gnawS in H1; auto. - intro H0; red; rewrite <- but_last_app; apply path_toS_app with one; auto. + left; split; auto; discriminate. + rewrite <- H0; apply gnawS_path_toS. * destruct s. -- now destruct H. -- discriminate. * rewrite H0; discriminate. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)