proposition: Lemma l11_28 : forall A B C D A' B' C', Cong_3 A B C A' B' C' -> Col A C D -> exists D', Cong A D A' D' /\ Cong B D B' D' /\ Cong C D C' D'.
proof: Proof. intros. induction (eq_dec_points A C). subst C. unfold Cong_3 in H. spliter. apply cong_symmetry in H1. apply cong_identity in H1. subst C'. induction(eq_dec_points A B). subst B. apply cong_symmetry in H2. apply cong_identity in H2. subst B'. assert(exists D', Cong A' D' A D). apply segment_construction_0. ex_and H1 D'. exists D'. apply cong_symmetry in H2. repeat split; assumption. induction (eq_dec_points A D). exists A'. subst D. repeat split. apply cong_trivial_identity. assumption. apply cong_trivial_identity. induction (eq_dec_points B D). subst D. exists B'. repeat split. assumption. apply cong_trivial_identity. assumption. assert(exists D'', CongA B A D B' A' D''). eapply angle_construction_3. auto. auto. intro. subst B'. apply cong_identity in H. contradiction. ex_and H5 D''. assert(exists D', Out A' D'' D' /\ Cong A' D' A D). apply segment_construction_3. unfold CongA in H6. spliter. auto. assumption. ex_and H5 D'. exists D'. repeat split. apply cong_symmetry. assumption. assert(CongA B A D B' A' D'). eapply (l11_10 B A D B' A' D''); try apply out_trivial; auto. intro. subst B'. unfold CongA in H6. spliter. absurde. apply l6_6. assumption. eapply (cong2_conga_cong _ A _ _ A' _). apply H8. assumption. Cong. Cong. unfold Cong_3 in H. spliter. induction(eq_dec_points A D). subst D. exists A'. repeat split. apply cong_trivial_identity. apply cong_commutativity. assumption. apply cong_commutativity. assumption. unfold Col in H0. induction H0. prolong A' C' D' C D. exists D'. repeat split. eapply (l2_11 A C D A' C' D'); try assumption. apply cong_symmetry. assumption. apply cong_commutativity. eapply (five_segment_with_def A C D B A' C' D' B'). repeat split; try assumption. apply cong_symmetry. assumption. apply cong_commutativity. assumption. assumption. apply cong_symmetry. assumption. induction H0. assert(exists D', Bet A' D' C' /\ Cong_3 A D C A' D' C'). eapply l4_5. apply between_symmetry. assumption. assumption. ex_and H5 D'. unfold Cong_3 in H6. spliter. exists D'. repeat split. assumption. apply cong_commutativity. eapply (l4_2 A D C B A' D' C' B'). repeat split; try assumption. apply between_symmetry. assumption. apply cong_commutativity. assumption. apply cong_commutativity. assumption. prolong C' A' D' A D. exists D'. repeat split. apply cong_symmetry. assumption. apply cong_commutativity. eapply (five_segment_with_def C A D B C' A' D' B'). repeat split; try assumption. apply between_symmetry. assumption. apply cong_commutativity. assumption. apply cong_symmetry. assumption. apply cong_commutativity. assumption. auto. eapply l2_11. apply between_symmetry. apply H0. apply H5. apply cong_commutativity. assumption. apply cong_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2