proposition: Lemma nf_of_finite : forall n b, nf (cons zero n b) -> b = zero.
proof: Proof. intros n b H; destruct b. - reflexivity. - apply nf_inv3 in H; case (not_lt_zero H);auto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)