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