proposition: Lemma l11_16 : forall A B C A' B' C', Per A B C -> A <> B -> C <> B -> Per A' B' C' -> A'<> B' -> C'<> B'-> CongA A B C A' B' C'.
proof: Proof. intros. prolong B C C0 B' C'. prolong B' C' C1 B C. prolong B A A0 B' A'. prolong B' A' A1 B A. unfold CongA. repeat split; try assumption. exists A0. exists C0. exists A1. exists C1. repeat split; try assumption. apply (l10_12 A0 B C0 A1 B' C1). apply (per_col _ _ C). intro;subst. auto. apply l8_2. apply (per_col _ _ A). auto. apply l8_2. assumption. unfold Col. left. assumption. unfold Col. left. assumption. 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. apply cong_right_commutativity. eapply l2_11. apply between_symmetry. apply H9. apply H11. apply cong_left_commutativity. assumption. apply cong_symmetry. apply cong_right_commutativity. assumption. apply cong_right_commutativity. eapply l2_11. apply H5. apply between_symmetry. apply H7. apply cong_symmetry. apply cong_left_commutativity. assumption. apply cong_right_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2