proposition: Lemma oplus_assoc (alpha beta gamma:T1) : nf alpha -> nf beta -> nf gamma -> alpha o+ (beta o+ gamma) = alpha o+ beta o+ gamma.
proof: Proof. Proof with eauto with T1. intros. apply oplus_assoc_0 with (T1.succ (max alpha (max beta gamma))); trivial. 1: apply succ_nf; repeat apply max_nf ... all: apply le_lt_trans with (max alpha (max beta gamma)); [| apply lt_succ] ... - apply le_max_a. - rewrite (max_comm alpha (max beta gamma)). rewrite <- max_assoc. apply le_max_a. - rewrite max_assoc. rewrite (max_comm (max alpha beta) gamma). apply le_max_a. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)