proposition: Lemma FinSubset_ball_triangle_r : forall e1 e2 x (l1 l2 : FinEnum), FinSubset_ball e1 x l1 -> (ball e2 l1 l2) -> FinSubset_ball (e1 + e2) x l2.
proof: Proof. intros e1 e2 x l1 l2 H1 [epos [H2 _]]. revert l2 H1 H2. induction l1; intros l2 H1 H2. exfalso; exact (FinSubset_ball_nil H1). unfold hemiMetric in *. apply FinSubset_ball_orC in H1. destruct H1 as [G | H1 | H1] using orC_ind. intro abs; contradict G; intro G; contradiction. assert (Z:InFinEnumC a (a :: l1)). { intro abs; contradict abs. exists a. split. left; reflexivity. reflexivity. } destruct (H2 a Z) as [ G | z [Hz0 Hz1]] using existsC_ind. intro abs; contradict G; intro G; contradiction. clear - H1 Hz0 Hz1. apply FinSubset_ball_closed. intros d dpos. apply FinSubset_ball_triangle_l with z. apply ball_triangle with a; assumption. apply FinSubset_ball_weak_le with (e1:=0). apply Qlt_le_weak, dpos. exact Hz0. apply IHl1. assumption. intros y Hy. apply H2. apply FinSubset_ball_cons. exact Hy. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength