proposition: Lemma Col_Col : forall A B C, Definitions.Col A B C <-> Col A B C.
proof: Proof. intros. unfold Definitions.Col, Col, BetS. simpl. unfold Definitions.BetS,eq. split. intros. destruct (eq_dec_points A B). left;auto. destruct (eq_dec_points A C). right;left;auto. destruct (eq_dec_points B C). right;right;left;auto. decompose [or] H. right;right;right;right;left;auto. right;right;right;right;right;Between. right;right;right;left;Between. intros. decompose [or] H;subst;spliter;Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates