proposition: Lemma mlarge_FS : forall i k, mlarge (FS i) (interval (S k) (S (i+k)%nat)).
proof: Proof. intro i. assert (FS i <> zero) by discriminate. generalize (L_fin_ok (S i)); intro H0. inversion H0. intro k; specialize (H2 k). unfold L_fin in H2. replace (Nat.pred (S i + S k))%nat with (S (i + k))%nat in H2; auto;abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)