proposition: Lemma le_anti_symmetry : forall A B C D, Le A B C D -> Le C D A B -> Cong A B C D.
proof: Proof. intros. assert (exists T, Bet C D T /\ Cong C T A B) by (apply l5_5_1;assumption). unfold Le in H. ex_and H Y. ex_and H1 T. assert (Cong C Y C T) by eCong. assert (Bet C Y T) by eBetween. assert (Y=T) by (eapply between_cong;eauto). subst Y. assert (T=D) by (eapply between_equality;eBetween). subst T. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col