fact: Definition pres_cong_line {Tm: Tarski_neutral_dimensionless} (f : @Tpoint Tn -> @Tpoint Tm) P Q := forall A B C D, Col P Q A -> Col P Q B -> Col P Q C -> Col P Q D -> Cong A B C D -> Cong (f A) (f B) (f C) (f D).
imports: GeoCoq.Tarski_dev.Definitions