proposition: Lemma gnaw_finite_1_iota : forall n i, gnaw (S n) (iota_from (S i) n) = 1.
proof: Proof. induction n. - now cbn. - intro i; specialize (IHn (S i)). rewrite <- FS_rw. rewrite <- succ_compat. simpl iota_from. rewrite gnaw_succ; auto with T1. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)