proposition: Lemma image_in_col : forall A B P P' Y : Tpoint, ReflectL_at Y P P' A B -> Col P P' Y.
proof: Proof. intros. unfold ReflectL_at in *. spliter. assert_cols. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop