proposition: Lemma cop_osp__ex_cop2 : forall A B C D E P, Coplanar A B C P -> OSP A B C D E -> exists Q, Coplanar A B C Q /\ Coplanar D E P Q /\ P <> Q.
proof: Proof. intros A B C D E P HCop HOSP. destruct (col_dec D E P) as [|HNCol]. { apply osp_distincts in HOSP; spliter. destruct (eq_dec_points P A). subst; exists B; repeat split; Cop. exists A; repeat split; Cop. } destruct (segment_construction E P P E) as [E' []]. assert (~ Col D E' P) by (intro; apply HNCol; ColR). destruct (cop_tsp__ex_cop2 A B C D E' P) as [Q [HQ1 [HQ2 HPQ]]]; [assumption|..]. { apply l9_41_2 with E. assert_diffs; destruct HOSP as [F [_ [HE]]]; apply bet_cop__tsp with P; Cop. apply osp_symmetry, HOSP. } exists Q; repeat split; auto. apply coplanar_perm_2, coplanar_trans_1 with E'; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar