proposition: Lemma orth_at__ncop2 : forall A B C U V X, V <> X -> Orth_at X A B C U V -> ~ Coplanar A B C V.
proof: Proof. intros A B C U V X HUX HOrth. apply orth_at__ncop1 with U X; [assumption|apply orth_at_symmetry, HOrth]. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2