proposition: Lemma concy_3 : forall (CONCY : cartesianPower Tpoint 4) (NOT_COL : cartesianPower Tpoint 3), pred_conj concy CONCY NOT_COL -> app not_col NOT_COL -> app concy CONCY.
proof: Proof. unfold pred_conj, app_2_n, concy; simpl. intros CONCY NOT_COL HConcy HNot_Col. destruct HConcy as [HConcy1 [HConcy2 [HConcy3 HConcy4]]]. apply concyclic_gen_pseudo_trans with (fst NOT_COL) (fst (snd NOT_COL)) (snd (snd NOT_COL)); try apply concyclic_gen_perm_1; auto. Qed.
imports: GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tarski_dev.Annexes.inscribed_angle