proposition: Lemma L_fin_ok i : L_spec (\F i) (L_fin i).
proof: Proof. induction i. - left; reflexivity. - apply L_spec_compat with (L_succ (L_fin i)). change (\F (S i)) with (FS i); rewrite <- succ_compat. destruct i. + simpl. unfold L_succ, L_fin; right. * discriminate. * intro k; red; simpl. rewrite interval_singleton; left. -- discriminate. -- split; [ discriminate | reflexivity]. + apply L_succ_ok; auto with T1. apply L_finS_S_le. + intros ; unfold L_fin, L_succ; abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)