proposition: Lemma F_not_lim : forall n, ~ is_limit (fin n).
proof: Proof. destruct n;red;inversion 1. decompose [or] H3; lt_clean. case zero_not_lim;auto. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)