proposition: Lemma cop3_osp__osp : forall A B C D E F P Q, ~ Col D E F -> Coplanar A B C D -> Coplanar A B C E -> Coplanar A B C F -> OSP A B C P Q -> OSP D E F P Q.
proof: Proof. intros A B C D E F P Q HNCol HD HE HF [R []]. exists R; split; apply (cop3_tsp__tsp A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar