proposition: Lemma col__image_spec : forall A B X, Col A B X -> ReflectL X X A B.
proof: Proof. intros. unfold ReflectL. split. exists X. split. apply l7_3_2. assumption. right. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop