proposition: Lemma cong_transitivity : forall A B C D E F : Tpoint, Cong A B C D -> Cong C D E F -> Cong A B E F.
proof: Proof. intros. eapply cong_inner_transitivity; eauto using cong_symmetry. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish