proposition: Lemma Rball_eq_trans: forall c r f g h, Rball_eq c r f g -> Rball_eq c r g h -> Rball_eq c r f h.
proof: Proof. unfold Rball_eq ; intros ; transitivity (g x) ; auto. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics