proposition: Lemma concy_perm_2 : forall (A B : Tpoint) (X : cartesianPower Tpoint 2), app_2_n concy A B X -> app_2_n concy B A X.
proof: Proof. unfold app_2_n, concy; simpl; intros; apply concyclic_gen_perm_2; auto. Qed.
imports: GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tarski_dev.Annexes.inscribed_angle