proposition: Lemma ex_diff_cop : forall A B C D, exists E, Coplanar A B C E /\ D <> E.
proof: Proof. intros A B C D. destruct (eq_dec_points A D); [destruct (eq_dec_points B D); subst|]. - destruct (another_point D) as [E]; exists E; split; Cop. - exists B; split; Cop. - exists A; split; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar