proposition: Lemma cong_diff_3 : forall A B C D , C <> D -> Cong A B C D -> A <> B.
proof: Proof. intros. intro;subst. apply H. eauto using cong_identity, cong_symmetry. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish