proposition: Lemma ball_sym e: Symmetric (ball e).
proof: Proof. Proof with auto. unfold Symmetric, ball. intros. destruct H as [qpos H]. split. exact qpos. rewrite distance_sym... Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith