proposition: Lemma all_coplanar : forall A B C D, Coplanar A B C D.
proof: Proof. apply upper_dim_implies_all_coplanar; unfold upper_dim_axiom; apply upper_dim. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity