proposition: Lemma cop3_orth_at__orth_at : forall A B C D E F U V X, ~ Col D E F -> Coplanar A B C D -> Coplanar A B C E -> Coplanar A B C F -> Orth_at X A B C U V -> Orth_at X D E F U V.
proof: Proof. intros A B C D E F U V X HNCol HD HE HF [HNCol1 [HUV [HX1 [HX2 HX3]]]]. repeat split; trivial. apply coplanar_pseudo_trans with A B C; assumption. assert (HCop : forall M, Coplanar A B C M -> Coplanar D E F M); [intro; apply coplanar_pseudo_trans; Cop|]; assert (forall M, Coplanar D E F M -> Coplanar A B C M); [intro; apply coplanar_pseudo_trans; auto with cop cop_perm| intros; apply HX3; auto]. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2