proposition: Lemma l11_18_2 : forall A B C D, Bet C B D -> CongA A B C A B D -> Per A B C.
proof: Proof. intros. unfold CongA in H0. spliter. ex_and H4 A0. ex_and H5 C0. ex_and H4 A1. ex_and H5 D0. assert (A0 = A1). apply (construction_uniqueness B A B A); auto. subst A1. assert(Per A0 B C0). unfold Per. exists D0. repeat split. eapply outer_transitivity_between2. apply between_symmetry. apply H6. eapply outer_transitivity_between. apply H. assumption. auto. assumption. eapply l2_11. apply between_symmetry. apply H6. apply H10. apply cong_left_commutativity. assumption. apply cong_symmetry. apply cong_right_commutativity. assumption. assumption. apply (per_col _ _ C0). intro. subst C0. apply between_identity in H6. subst C. absurde. apply l8_2. apply (per_col _ _ A0). intro. subst A0. apply between_identity in H8. subst A. absurde. apply l8_2. assumption. unfold Col. right; left. apply between_symmetry. assumption. unfold Col. right; left. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2