proposition: Lemma largeS_iff (alpha : T1) (s : list nat) : largeS alpha s <-> gnawS alpha s = T1.zero.
proof: Proof. unfold largeS, largeSb; destruct (gnawS alpha s). - split;auto. - split; discriminate. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)