proposition: Lemma ex_ncol_cop : forall A B C D E, D <> E -> exists F, Coplanar A B C F /\ ~ Col D E F.
proof: Proof. intros A B C D E HDE. destruct (col_dec A B C) as [|HNCol]. destruct (not_col_exists D E HDE) as [F]; exists F; split; Cop. destruct (col_dec D E A); [destruct (col_dec D E B)|]. - exists C; split; Cop. intro; apply HNCol; ColR. - exists B; split; Cop. - exists A; split; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar