proposition: Lemma genball_triangle (e1 e2: Qinf) (a b c: X): genball e1 a b → genball e2 b c → genball (e1 + e2) a c.
proof: Proof. Proof with auto. intros U V. destruct e1 as [e1|]... destruct e2 as [e2|]... apply genball_alt. apply genball_alt in U. apply genball_alt in V. destruct (Qdec_sign (e1 + e2)) as [[G | I] | J]; destruct (Qdec_sign e1) as [[A | B] | C]; destruct (Qdec_sign e2) as [[D | E] | F]; intuition. revert G. apply (Qlt_is_antisymmetric_unfolded _ _)... revert G. rewrite F, Qplus_0_r. apply (Qlt_is_antisymmetric_unfolded _ _ B)... revert G. rewrite C, Qplus_0_l. apply (Qlt_is_antisymmetric_unfolded _ _ E)... revert G. rewrite C, F. apply Qlt_irrefl. change (genball (exist _ e1 B + exist _ e2 E )%Qpos a c). apply ball_genball. apply Rtriangle with b; apply ball_genball... rewrite <- V. assert (e1 + e2 == e1) by (rewrite F, Qplus_0_r; reflexivity). apply (genball_Proper (e1+e2) e1 H2 a a (reflexivity _) b b (reflexivity _)), U. rewrite U. assert (e1 + e2 == e2) by (rewrite C, Qplus_0_l; reflexivity). apply (genball_Proper (e1+e2) e2 H2 b b (reflexivity _) c c (reflexivity _)), V. rewrite U, V. apply genball_Reflexive. apply Qlt_le_weak, I. exfalso. apply Qlt_le_weak in E. apply (Qplus_lt_le_compat _ _ _ _ B) in E. rewrite J in E. apply (Qlt_irrefl 0 E). exfalso. rewrite F, Qplus_0_r in J. rewrite J in B. exact (Qlt_irrefl 0 B). exfalso. rewrite C, Qplus_0_l in J. rewrite J in E. exact (Qlt_irrefl 0 E). Qed.
imports: CoRN.algebra.RSetoid Arith List CoRN.model.totalorder.QposMinMax CSetoids Qmetric Qring Qinf QnnInf QnonNeg ProductMetric QposInf Qposclasses UniformContinuity MathClasses.implementations.stdlib_rationals stdlib_omissions.Pair stdlib_omissions.Q PointFree MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.theory.products