proposition: Lemma o_finite_mult_lt_phi0_1 : forall a b n, T1.lt a b -> T1.lt (o_finite_mult n (phi0 a)) (phi0 b).
proof: Proof. Proof with auto with T1. intros a b n H;destruct n. - apply zero_lt. - rewrite o_finite_mult_rw. now apply head_lt. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)