proposition: Lemma conga_trans : forall A B C A' B' C' A'' B'' C'', CongA A B C A' B' C' -> CongA A' B' C' A'' B'' C'' -> CongA A B C A'' B'' C''.
proof: Proof. intros. assert (HH:=H). unfold CongA in H. spliter. ex_and H4 A0. ex_and H5 C0. ex_and H4 A1. ex_and H5 C1. assert_diffs. assert(A'' <> B'' /\ C'' <> B''). unfold CongA in H0. spliter. split; assumption. spliter. assert(CongA A1 B' C1 A'' B'' C'') by (apply l11_10 with A' C' A'' C'';Out). assert (CongA A0 B C0 A' B' C') by (apply l11_10 with A C A' C';Out). assert (Cong B A0 B' A1). { apply cong_right_commutativity. apply l2_11 with A A'; Between; Cong. } assert (Cong B C0 B' C1). { apply cong_right_commutativity. apply l2_11 with C C'; Between; Cong. } assert (Cong A0 C0 A1 C1). { apply (l11_4_1) in H24. spliter. apply H30. repeat split;Between. } assert (Cong_3 A0 B C0 A1 B' C1) by (repeat split; Cong). apply cong3_symmetry in H28. assert (CongA A0 B C0 A'' B'' C'') by (eauto using cong3_conga2). apply l11_10 with A0 C0 A'' C''; Out. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2