proposition: Lemma oplus_comm (alpha beta: T1): nf alpha -> nf beta -> alpha o+ beta = beta o+ alpha.
proof: Proof. intros ? ?; apply oplus_comm_0 with (T1.succ (max alpha beta)); trivial. - apply succ_nf; apply max_nf;auto. - apply le_lt_trans with (max alpha beta); trivial. + apply le_max_a. + apply lt_succ. - apply le_lt_trans with (max alpha beta); trivial. + apply le_max_b. + apply lt_succ. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)