proposition: Lemma triangle_inequality : forall A B C D, Bet A B D -> Cong B C B D -> Le A C A D.
proof: Proof. intros A B C D HCong HBet. elim(bet_dec A B C). - intro. elim(eq_dec_points A B). intro; subst; Le. intro. assert(C = D). apply (construction_uniqueness A B B D); Cong. subst; Le. - intro. assert(Hlt := triangle_strict_inequality A B C D). destruct Hlt; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2