proposition: Lemma large_iff (alpha : T1) (s : list nat) : large alpha s <-> gnaw alpha s = 0.
proof: Proof. unfold large, largeb; destruct (gnaw alpha s). - split;auto. - split; discriminate. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)