proposition: Lemma largeb_finite : forall n i, largeb (S n) (iota_from (S i) (S n)) = true.
proof: Proof. intros; unfold largeb; now rewrite gnaw_finite. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)