proposition: Lemma image_triv : forall A B, Reflect A A A B.
proof: Proof. intros. induction (eq_dec_points A B). right; split; Midpoint. left; split. auto. apply col__image_spec; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop