proposition: Lemma gnaw_omega_n_SSn : forall n, gnaw T1omega (iota_from (S n) (S (S n))) = zero.
proof: Proof. intro n; destruct n. - reflexivity. - apply gnaw_finite. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)