proposition: Lemma orth_at__ncop1 : forall A B C U V X, U <> X -> Orth_at X A B C U V -> ~ Coplanar A B C U.
proof: Proof. intros A B C U V X HUX HOrth HCop. apply HUX, eq_sym, (col_cop_orth_at__eq A B C U V); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2