proposition: Lemma concyclic_gen_1123 : forall A B C, Concyclic_gen A A B C.
proof: Proof. unfold Concyclic_gen; simpl; intros A B C. elim (col_dec A B C); intro; [right; repeat split; Col|]. left. split; Cop. destruct (triangle_circumscription A B C H) as [O]; spliter. exists O, A; unfold OnCircle; repeat split; Cong. Qed.
imports: GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tarski_dev.Annexes.inscribed_angle