proposition: Lemma inangle__coplanar : forall A B C D, InAngle A B C D -> Coplanar A B C D.
proof: Proof. intros A B C D H. unfold InAngle in H; spliter. destruct H2 as [X [HBet Dij]]. exists X; right; left. split; Col. induction Dij; [subst|]; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality