proposition: Lemma cop3_osp__os : forall A B C D E X Y, D <> E -> Coplanar A B C D -> Coplanar A B C E -> Coplanar D E X Y -> OSP A B C X Y -> OS D E X Y.
proof: Proof. intros A B C D E X Y HDE HD HE HCop HOSP. assert (HX : ~ Coplanar A B C X) by (apply osp__ncop1 with Y, HOSP). assert (HY : ~ Coplanar A B C Y) by (apply osp__ncop2 with X, HOSP). apply cop_nts__os. assumption. intro; apply HX, col_cop2__cop with D E; Col. intro; apply HY, col_cop2__cop with D E; Col. intro. apply osp__ntsp in HOSP. apply HOSP, cop2_ts__tsp with D E; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar