proposition: Lemma concy_perm_1 : forall (A : Tpoint) (X : cartesianPower Tpoint 3), app_1_n concy A X -> app_n_1 concy X A.
proof: Proof. unfold concy; simpl. intros; apply concyclic_gen_perm_1; auto. Qed.
imports: GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tarski_dev.Annexes.inscribed_angle