proposition: Lemma reflect__coplanar : forall A B C D, Reflect A B C D -> Coplanar A B C D.
proof: Proof. intros A B C D [[_ HR]|[Heq]]. apply reflectl__coplanar, HR. subst; apply coplanar_perm_16, coplanar_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality