proposition: Lemma plus_nf: forall a, nf a -> forall b, nf b -> nf (a + b).
proof: Proof. intros a Ha b Hb; case (lt_eq_lt_dec 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; try assumption; 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: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)