proposition: Lemma cong2_conga_cong : forall A B C A' B' C', CongA A B C A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
proof: Proof. intros. unfold CongA in H. spliter. ex_and H5 A0. ex_and H6 C0. ex_and H5 A1. ex_and H6 C1. assert(Cong A C0 A' C1). eapply (l4_2 B A A0 C0 B' A' A1 C1). repeat split; try assumption. eapply l2_11. apply H5. apply H9. apply cong_commutativity. assumption. eapply cong_transitivity. apply H6. apply cong_commutativity. apply cong_symmetry. apply cong_transitivity with A B; Cong. eapply cong_transitivity. apply H6. apply cong_commutativity. apply cong_symmetry. apply cong_transitivity with A B; Cong. eapply cong_transitivity. eapply l2_11. apply H7. apply H11. assumption. eapply cong_transitivity. apply H8. apply cong_symmetry. eapply cong_transitivity. apply H12. assumption. apply cong_reflexivity. apply cong_commutativity. eapply (l4_2 B C C0 A B' C' C1 A'). repeat split; try assumption. eapply l2_11. apply H7. apply H11. assumption. eapply cong_transitivity. apply H8. eapply cong_transitivity. apply cong_symmetry. apply H1. apply cong_symmetry. assumption. eapply cong_transitivity. apply H8. eapply cong_transitivity. apply cong_symmetry. apply H1. apply cong_symmetry. assumption. apply cong_commutativity. assumption. apply cong_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2