proposition: Lemma cong3_conga : forall A B C A' B' C', A <> B -> C <> B -> Cong_3 A B C A' B' C' -> CongA A B C A' B' C'.
proof: Proof. intros. assert (A' <> B') by (eauto using cong3_diff). assert (B' <> C') by (eauto using cong3_diff2). apply (l11_3_bis A B C A' B' C'). exists A, C, A', C'. intuition Out. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2