proposition: Lemma cong_symmetry : forall A B C D : Tpoint, Cong A B C D -> Cong C D A B.
proof: Proof. intros. eapply cong_inner_transitivity. apply H. apply cong_reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish