proposition: Lemma oplus_lt_phi0 : forall a b c, nf a -> nf b -> nf c -> T1.lt a c -> T1.lt b c -> T1.lt (phi0 a o+ phi0 b) (phi0 c).
proof: Proof. intros; rewrite oplus_cons_cons; case_eq (compare a b). rewrite oplus_0_r; cbn. all: intros; apply head_lt; eauto with T1. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)