proposition: Lemma cong3_conga2 : forall A B C A' B' C' A'' B'' C'', Cong_3 A B C A' B' C' -> CongA A B C A'' B'' C'' -> CongA A' B' C' A'' B'' C''.
proof: Proof. intros. unfold CongA in H0. spliter. ex_and H4 A0. ex_and H5 C0. ex_and H4 A2. ex_and H5 C2. unfold Cong_3 in H. spliter. unfold CongA. assert_diffs. repeat split; auto. prolong B' A' A1 B'' A''. prolong B' C' C1 B'' C''. exists A1, C1, A2, C2. repeat split;try assumption. apply cong_transitivity with B A; Cong. apply cong_transitivity with B C; auto. assert (Cong A A0 A' A1). apply cong_transitivity with B'' A''; Cong. assert(Cong B A0 B' A1). apply l2_11 with A A'; Cong. assert (Cong C C0 C' C1). apply cong_transitivity with B'' C''; Cong. assert(Cong B C0 B' C1). eapply l2_11 with C C'; auto. assert(FSC B A A0 C B' A' A1 C'). unfold FSC; assert_cols; repeat split; Cong. assert(Cong A0 C A1 C'). eauto using l4_16. apply cong_commutativity. assert(Cong C0 A0 C1 A1). apply (l4_16 B C C0 A0 B' C' C1 A1). unfold FSC;assert_cols;repeat split; Cong. auto. apply cong_transitivity with A0 C0; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2