proposition: Lemma par_trans__par_dec : postulate_of_transitivity_of_parallelism -> decidability_of_parallelism.
proof: Proof. intros HTP A B C D. elim (eq_dec_points A B); intro HAB; [treat_equalities; right; intro; assert_diffs; auto|]. elim (eq_dec_points C D); intro HCD; [treat_equalities; right; intro; assert_diffs; auto|]. destruct (parallel_existence1 A B C HAB) as [D' HPar]. elim (col_dec C D D'); intro HCol; [left; apply par_col_par with D'; Par; Col| right; intro; apply HCol, par_id, HTP with A B; Par]. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel