proposition: Lemma not_col_perm_2 : forall A B (X : cartesianPower Tpoint 1), app_2_n not_col A B X -> app_2_n not_col B A X.
proof: Proof. unfold not_col, app_2_n; simpl; Col. Qed.
imports: GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tarski_dev.Annexes.inscribed_angle