proposition: Lemma ap_plus : forall a, ap a -> forall b c, nf b -> nf c -> b < a -> c < a -> b + c < a.
proof: Proof. destruct 1. intro b; elim b. intro c; elim c;intros. simpl; auto with T1. simpl. auto. intros c H0. intros. generalize c0 H2 H4. destruct c1. rewrite (plus_a_zero). auto. auto. intros. case (trichotomy_inf c c1_1). destruct 1. rewrite (plus_cons_cons_rw1 n t n0 c1_2 l). auto. subst c1_1. rewrite (plus_cons_cons_rw2 H1 H5). constructor 2. inversion H3;auto. inversion H8. inversion H8. intro H7. rewrite (plus_cons_cons_rw3). constructor 2. inversion_clear H3;auto. inversion H8. inversion H8. auto. auto. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List