proposition: Lemma circle_cases : forall O P X, OnCircle X O P \/ InCircleS X O P \/ OutCircleS X O P.
proof: Proof. intros O P X. destruct (cong_dec O X O P); auto. right. destruct (le_cases O P O X); [right|left]; split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel