proposition: Lemma upper_dim_implies_per2__col : upper_dim_axiom -> (forall A B C X, Per A X C -> X <> C -> Per B X C -> Col A B X).
proof: Proof. intros HUD A B C X HPer1 HDiff HPer2. destruct HPer1 as [C' HPer1]. destruct HPer2 as [C'' HPer2]. assert (C' = C'') by (apply symmetric_point_uniqueness with C X; spliter; auto); treat_equalities. unfold upper_dim_axiom in HUD. spliter; assert_diffs; unfold Midpoint in *; spliter; apply HUD with C C'; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane