proposition: Lemma col_perm_2 : forall A B (X : cartesianPower Tpoint 1), app_2_n col A B X -> app_2_n col B A X.
proof: Proof. unfold col. unfold app_2_n. simpl. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tactics.Coinc.tactics_axioms