proposition: Lemma col_cop__cop : forall A B C D E, Coplanar A B C D -> C <> D -> Col C D E -> Coplanar A B C E.
proof: Proof. intros A B C D E HCop HCD HCol. destruct (col_dec D A C). assert (Col A C E) by (apply l6_16_1 with D; Col); Cop. apply coplanar_perm_2, (coplanar_trans_1 D); Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar