proposition: Lemma upper_dim_implies_all_coplanar : upper_dim_axiom -> all_coplanar_axiom.
proof: Proof. intro HUD; unfold all_coplanar_axiom; intros. elim (col_dec A B C); Cop; intro HABC. elim (col_dec A B D); Cop; intro HABD. elim (col_dec A C D); Cop; intro HACD. elim (upper_dim_implies_one_or_two_sides HUD A B C D); Col; [apply ts__coplanar|apply os__coplanar]. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane