proposition: Lemma Lemma4_4 : largeS beta s.
proof: Proof. specialize (@Lemma_4_4_1 s n alpha beta Halpha Hbeta Hs H); intro H1. repeat red in H0; unfold largeSb in H0; destruct (gnawS alpha s). - apply const_pathS_eps_zero in H1; now rewrite largeS_iff. - discriminate. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)