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