proposition: Lemma neqc_chara : forall A B C D, A <> B -> ~ EqC A B C D <-> (exists X, OnCircle X A B /\ ~ OnCircle X C D).
proof: Proof. intros A B C D HAB. split. { intro Hneq. destruct (eq_dec_points C A) as [|HCA]. { destruct (cong_dec A B C D) as [|HNCong]. exfalso; apply Hneq, eqc_chara; split; auto. subst C; exists B; split; Circle. } destruct (tree_points_onc_cop2 A B C HAB) as [B0 [B1 [B2]]]; spliter. destruct (cong_dec C B0 C D); [destruct (cong_dec C B1 C D);[destruct (cong_dec C B2 C D)|]|]. - exfalso. apply HCA. apply cong2_cop2_onc3__eq with B B0 B1 B2; auto; apply cong_transitivity with C D; Cong. - exists B2; auto. - exists B1; auto. - exists B0; auto. } intros [X [HX Habs]] Heq. apply Habs, Heq, HX. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel