proposition: Lemma orth_dec : forall A B C U V, Orth A B C U V \/ ~ Orth A B C U V.
proof: Proof. intros A B C U V. destruct (eq_dec_points U V). unfold Orth, Orth_at; right; intros [X []]; spliter; auto. revert dependent V. revert U. assert (Haux : forall U V, U <> V -> ~ Coplanar A B C U -> Orth A B C U V \/ ~ Orth A B C U V). { intros U V HUV HU. destruct (l11_62_existence_bis A B C U HU) as [X HX]. destruct (col_dec U V X). left; apply col_orth__orth with X; Col; apply orth_symmetry; exists X; apply HX. right; intros [Y HY]. assert (X = Y). { apply l11_62_unicity_bis with A B C U; [assumption|]. apply orth_at_symmetry, col_orth_at__orth_at with V; [destruct HY; spliter..|]; trivial. intro; subst Y; absurd (Coplanar A B C U); [|assumption]. assert_diffs; apply orth_at__ncop2 with X X; auto. } subst; destruct HY; spliter; Col. } intros U V HUV. destruct (col_dec A B C). unfold Orth, Orth_at; right; intros [X []]; spliter; auto. destruct (cop_dec A B C U); [|auto]. destruct (cop_dec A B C V). - right; intro. apply HUV, (orth_at2__eq A B C U V); apply col_cop_orth__orth_at; Col. - destruct (Haux V U) as [HOrth|HNOrth]; auto; [left|right; intro HOrth; apply HNOrth]; apply orth_symmetry, HOrth. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2