proposition: Lemma conga_sym : forall A B C A' B' C', CongA A B C A' B' C' -> CongA A' B' C' A B C.
proof: Proof. unfold CongA. intros. spliter. ex_and H3 A0. ex_and H4 C0. ex_and H3 D0. ex_and H4 F0. repeat split; try assumption. exists D0. exists F0. exists A0. exists C0. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2