proposition: Lemma par_dec_NID : decidability_of_parallelism <-> decidability_of_not_intersection.
proof: Proof. split; intros Hdec A B C D; destruct (cop_dec A B C D) as [|HNCop]. - destruct (Hdec A B C D) as [[HParS|Heq]|HNPar]. * left; unfold Par_strict in HParS; spliter; assumption. * right; intro Habs; apply Habs; exists B; spliter; Col. * right; intro Habs. destruct (eq_dec_points A B). apply Habs; exists C; subst; split; Col. destruct (eq_dec_points C D). apply Habs; exists A; subst; split; Col. apply HNPar; left; unfold Par_strict; repeat split; assumption. - left; intros [I []]; apply HNCop; exists I; left; split; Col. - destruct (eq_dec_points A B). right; subst; intro; assert_diffs; auto. destruct (eq_dec_points C D). right; subst; intro; assert_diffs; auto. destruct (col_dec A C D). { destruct (col_dec B C D). left; right; repeat split; assumption. right; intros [[_ Habs]|]. apply Habs; exists A; split; Col. spliter; auto. } destruct (Hdec A B C D) as [HPar|HNPar]. left; left; repeat split; assumption. right. intros [HParS|Heq]. apply HNPar; unfold Par_strict in HParS; spliter; assumption. spliter; auto. - right; intro HPar; apply HNCop, par__coplanar, HPar. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel