proposition: Lemma ex_ncol_cop2 : forall A B C D, exists E F, Coplanar A B C E /\ Coplanar A B C F /\ ~ Col D E F.
proof: Proof. intros A B C D. destruct (ex_diff_cop A B C D) as [E [HE HDE]]. destruct (ex_ncol_cop A B C D E HDE) as [F []]. exists E, F; repeat split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar