proposition: Lemma o_finite_mult_nf : forall a n, nf a -> nf (o_finite_mult n a).
proof: Proof. induction n;simpl. - constructor. - intro;apply oplus_nf; auto. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)