proposition: Lemma not_conga : forall A B C A' B' C' D E F , CongA A B C A' B' C' -> ~ CongA A B C D E F -> ~ CongA A' B' C' D E F.
proof: Proof. intros. intro. apply H0. eapply conga_trans. apply H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2