proposition: Lemma ball_triangle (e1 e2 : Q) a b c : ball e1 a b -> ball e2 b c -> ball (e1+e2) a c.
proof: Proof. Proof with auto. unfold ball. intros. destruct H, H0. assert (Qle 0 (e1+e2)). { apply (Qle_trans _ (e1+0)). rewrite Qplus_0_r. exact H. apply Qplus_le_r. exact H0. } split. exact H3. apply CRle_trans with (distance a b + distance b c). apply distance_triangle. rewrite <- CRplus_Qplus. apply CRplus_le_compat; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith