proposition: Lemma same_dir_dec : forall A B C D, Same_dir A B C D \/ ~ Same_dir A B C D.
proof: Proof. intros. unfold Same_dir. unfold EqV. elim (eq_dec_points A B); intro HAB; elim (eq_dec_points C D); intro HCD; try tauto. right; intro HFalse. elim HFalse; clear HFalse; intro HFalse. spliter; intuition. destruct HFalse as [E [HFalse HElim]]. elim HElim; clear HElim; intro HElim. subst. apply plg_cong in HElim. destruct HElim as [HCong1 HCong2]. treat_equalities. apply out_diff2 in HFalse; intuition. destruct HElim as [Hclear HCE]; clear Hclear; subst. apply out_diff2 in HFalse; intuition. right; intro HFalse. elim HFalse; clear HFalse; intro HFalse. spliter; intuition. destruct HFalse as [E [HFalse Hclear]]; clear Hclear. subst. apply out_diff1 in HFalse; intuition. assert (H := plg_existence B A C). assert (HPar : B <> A) by auto. apply H in HPar; clear H. destruct HPar as [E HPar]. elim (out_dec C D E); intro Hout. left. right. exists E. split; try assumption. left. apply plg_comm2 in HPar. assumption. right. intro H. elim H; clear H; intro H. spliter; subst; intuition. destruct H as [F [Hout' HElim]]. elim HElim; clear HElim; intro HElim. apply plg_comm2 in HElim. assert (HEF := plg_uniqueness B A C E F HPar HElim). subst; intuition. spliter; intuition. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec