proposition: Lemma col2_cop__cop : forall A B C D E F, Coplanar A B C D -> C <> D -> Col C D E -> Col C D F -> Coplanar A B E F.
proof: Proof. intros A B C D E F HCop HCD HE HF. destruct (eq_dec_points E C). subst; apply col_cop__cop with D; Col; Cop. apply col_cop__cop with C; [apply coplanar_perm_1, col_cop__cop with D| |apply l6_16_1 with D]; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar