proposition: Lemma ex_perp_cop : forall A B C P, A <> B -> exists Q, Perp A B Q C /\ Coplanar A B P Q.
proof: Proof. intros A B C P HAB. destruct (col_dec A B C) as [HCol|HNCol]; [destruct (col_dec A B P) as [|HNCol]|]. - destruct (not_col_exists A B HAB) as [P' HNCol]. destruct (l10_15 A B C P' HCol HNCol) as [Q []]. exists Q. split; trivial. exists P; left; Col. - destruct (l10_15 A B C P HCol HNCol) as [Q []]. exists Q. split; [|apply os__coplanar]; assumption. - destruct (l8_18_existence A B C HNCol) as [Q []]. exists Q. split. Perp. exists Q; left; split; Col. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity