proposition: Lemma conga_diff45 : forall A B C A' B' C', CongA A B C A' B' C' -> A' <> B'.
proof: Proof. intros A B C A' B' C' H. apply (conga_diff1 A' B' C' A B C); apply conga_sym; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2