proposition: Lemma LT_inv : forall a n l l', LT l' ((a,n)::l) -> l' = nil \/ (exists b p l'', l'= ((b,p)::l'') /\ ltA b a) \/ (exists l'', l'=(a,n)::l'' /\ LT l'' l) \/ (exists p l'', l'= ((a,p)::l'') /\ p < n).
proof: Proof. destruct 1. destruct l'. - now left. - right. destruct H0 as [H0 H1]; inversion H0. + subst; right; right; exists n0, l'; split; auto. + subst; left; exists a0, n0, l'; split; auto. + subst; right;left; exists l'; split; auto. split; auto. eapply NF_inv1 ; eauto. split; auto. eapply NF_inv1 ; eauto. Qed.
imports: Relations List Sorted Arith hydras(Restriction) Coq(Lia)