proposition: Lemma L_spec_inv2 alpha f : L_spec alpha f -> alpha <> zero -> (forall k, mlarge alpha (interval (S k) (Nat.pred (f (S k))))).
proof: Proof. inversion_clear 1; [now destruct 1 | auto]. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)