proposition: Lemma triangle_inequality1 : forall A B C D E, SumS A B B C D E -> Le A C D E.
proof: Proof. intros A B C D E HSum. destruct (segment_construction A B B C) as [D' [HBet HCong]]. apply (l5_6 A C A D'); Cong. apply triangle_inequality with B; Cong. apply (sums2__cong56 A B B C); trivial. exists A, B, D'; repeat split; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv