proposition: Lemma gnaw_omega_1 (n:nat) : gnaw T1omega (interval (S n) (S n + n)%nat) = 1.
proof: Proof. unfold interval. replace (S (S n + n) - S n)%nat with (S n). destruct n. - reflexivity. - apply gnaw_finite_1_iota. - simpl; destruct n. + reflexivity. + abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)