proposition: Lemma L_pos_inv alpha f : alpha <> zero -> L_spec alpha f -> forall k, (S k < f (S k))%nat.
proof: Proof. destruct alpha; [now destruct 1 | intros _ H]. inversion_clear H as [H0 H1 |]. intro k; specialize (H1 k). generalize (path_to_not_nil H1); intro H2. rewrite interval_not_empty_iff in H2; abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)