proposition: Lemma finite_lt : forall n p : nat, (n < p)%nat -> F n < F p.
proof: Proof. destruct n;simpl. destruct p. inversion 1. simpl;auto with T1. destruct p. inversion 1. simpl;auto with T1. intro; assert (n<p)%nat ; auto with arith T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List