proposition: Lemma is_image_spec_dec : forall A B C D, ReflectL A B C D \/ ~ ReflectL A B C D.
proof: Proof. intros. elim (eq_dec_points C D); intro HCD. subst. elim (eq_dec_points A B); intro HAB. subst. left. apply image_spec_triv. right. intro H. unfold ReflectL in *. destruct H as [H HFalse]. elim HFalse; clear HFalse; intro HFalse. apply perp_distinct in HFalse. intuition. intuition. elim (l10_6_existence_spec C D A HCD); intros B' HB'. elim (eq_dec_points B B'); intro HBB'. subst. tauto. right. intro H. apply HBB'. apply l10_6_uniqueness with C D A. unfold Reflect. tauto. unfold Reflect. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop