proposition: Lemma finite_ltR : forall n p : nat, F n < F p -> (n < p)%nat.
proof: Proof. destruct n;simpl. destruct p. inversion 1. auto with arith. destruct p. inversion 1. simpl. intro H; case (lt_inv_nb H). auto with arith. intros (_,H0); case (lt_irr H0). Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List