proposition: Lemma eqc_chara: forall A B C D, EqC A B C D <-> A = C /\ Cong A B C D.
proof: Proof. intros A B C D. split. - intro Heq. unfold EqC in Heq. assert (C = A). { destruct (eq_dec_points A B) as [|Hd]. - subst B. unfold OnCircle in Heq. assert (Cong A D A A) by (rewrite Heq; Cong). treat_equalities. destruct (segment_construction A C A C) as [A' []]. assert (Cong A A' A A) by (rewrite Heq; Cong). treat_equalities; auto. - destruct (tree_points_onc_cop2 A B C Hd) as [B0 [B1 [B2]]]. spliter. assert (HCong := onc2__cong C D). apply cong2_cop2_onc3__eq with B B0 B1 B2; try (apply HCong; apply Heq); auto. } subst C. split; trivial. unfold OnCircle in Heq. rewrite <- (Heq B); Cong. - intros []. subst C. intro X. split; intro; [apply cong_transitivity with A B|apply cong_transitivity with A D]; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel