proposition: Lemma InPlane'__Coplanar : forall A B C P, InPlane' P A B C -> Coplanar A B C P.
proof: Proof. intros A B C P [|[|]]; Cop; apply os__coplanar; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.coplanar GeoCoq.Tarski_dev.Ch09_plane