proposition: Lemma largeb_n_R : forall s n, ~ In 0 s -> (n < List.length s)%nat -> largeb (S n) s = true.
proof: Proof. intros; unfold largeb. rewrite gnaw_n_R; auto. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)