proposition: Lemma col_cop2__cop : forall A B C U V P, U <> V -> Coplanar A B C U -> Coplanar A B C V -> Col U V P -> Coplanar A B C P.
proof: Proof. intros A B C U V P HUV HU HV HCol. destruct (col_dec A B C) as [HCol1|HNCol]. apply col__coplanar, HCol1. revert dependent C. revert A B. assert (Haux : forall A B C, ~ Col A B C -> ~ Col U A B -> Coplanar A B C U -> Coplanar A B C V -> Coplanar A B C P). { intros A B C HNCol HNCol' HU HV. apply (coplanar_trans_1 U); [Cop..|]. apply coplanar_perm_12, col_cop__cop with V; auto. apply (coplanar_trans_1 C); Col; Cop. } intros A B C HU HV HNCol. destruct (col_dec U A B); [destruct (col_dec U A C)|]. - apply coplanar_perm_12, Haux; Col; Cop. intro; apply HNCol; destruct (eq_dec_points U A); ColR. - apply coplanar_perm_2, Haux; Col; Cop. - apply Haux; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar