proposition: Lemma plus_nf : forall a, nf a -> forall b, nf b -> nf (a + b).
proof: Proof. intros. case (trichotomy_inf a b). destruct 1. apply plus_nf0 with b; auto. apply lt_trans with b; auto. apply lt_a_phi0_a. apply lt_a_phi0_a. subst b. apply plus_nf0 with a; auto. apply lt_a_phi0_a. apply lt_a_phi0_a. intro; apply plus_nf0 with a; auto. apply lt_a_phi0_a. apply lt_trans with a. auto. apply lt_a_phi0_a. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List