proposition: Lemma l11_17 : forall A B C A' B' C', Per A B C -> CongA A B C A' B' C' -> 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 C1. assert (Per A0 B C0). apply (per_col _ _ C). auto. apply l8_2. apply (per_col _ _ A). auto. apply l8_2. assumption. unfold Col. left. assumption. unfold Col. left. assumption. assert(Per A1 B' C1). eapply l8_10. apply H13. repeat split. apply cong_right_commutativity. eapply l2_11. apply between_symmetry. apply H4. apply H8. apply cong_left_commutativity. assumption. apply cong_symmetry. apply cong_right_commutativity. assumption. assumption. apply cong_right_commutativity. eapply l2_11. apply H6. apply between_symmetry. apply H10. apply cong_left_commutativity. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_right_commutativity. assumption. apply (per_col _ _ C1). intro. subst C1. apply between_identity in H10. subst C'. absurde. apply l8_2. apply (per_col _ _ A1). intro. subst A1. 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