proposition: Lemma o_finite_mult_rw : forall a n, o_finite_mult (S n) (phi0 a) = cons a n T1.zero.
proof: Proof. induction n. - reflexivity. - change (phi0 a o+ (o_finite_mult (S n) (phi0 a)) = cons a (S n) T1.zero). rewrite IHn; rewrite oplus_eqn. simpl; now rewrite compare_refl. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)