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