proposition: Lemma cop_perm_2 : forall A B (X : cartesianPower Tpoint 2), app_2_n cop A B X -> app_2_n cop B A X.
proof: Proof. unfold cop. unfold app_2_n. simpl. Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tactics.Coinc.tactics_axioms