proposition: Lemma Rball_eq_sym: forall c r f g, Rball_eq c r f g -> Rball_eq c r g f.
proof: Proof. unfold Rball_eq ; intros ; symmetry ; auto. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics