proposition: Lemma oplus_nf (alpha beta : T1) : nf alpha -> nf beta -> nf (alpha o+ beta).
proof: Proof. intros H H0; apply oplus_nf_0 with (phi0 (max alpha beta)) ; trivial. - apply nf_phi0. apply max_nf; trivial. - apply lt_le_trans with (phi0 alpha). + apply lt_a_phi0_a. + apply phi0_mono, le_max_a. - rewrite max_comm. apply lt_le_trans with (phi0 beta). + apply lt_a_phi0_a. + apply phi0_mono, le_max_a. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)