proposition: Lemma cong_right_commutativity : forall A B C D, Cong A B C D -> Cong A B D C.
proof: Proof. intros. apply cong_symmetry. apply cong_symmetry in H. apply cong_left_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish