proposition: Lemma triangle_inequality_2 : forall A B C A' B' C', Bet A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Le A C A' C'.
proof: Proof. intros A B C A' B' C' HBet HCongA HCongB. destruct (segment_construction A B B C) as [D [HBetD HCongD]]. apply (l5_6 A C A D); Cong. apply (triangle_inequality _ B); Cong. apply (l2_11 _ B _ _ B'); Cong. apply cong_transitivity with B C; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2