proposition: Lemma per2__col : forall A B C X, Per A X C -> X <> C -> Per B X C -> Col A B X.
proof: Proof. apply upper_dim_implies_per2__col; unfold upper_dim_axiom; apply upper_dim. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity