proposition: Lemma diff_perm_2 : forall A B (X : cartesianPower Tpoint 0), app_2_n diff A B X -> app_2_n diff B A X.
proof: Proof. unfold diff. unfold app_2_n. simpl. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tactics.Coinc.tactics_axioms