proposition: Lemma inter_sym : forall A B C D X, Inter A B C D X -> Inter C D A B X.
proof: Proof. intros. unfold Inter in *. spliter. ex_and H0 P. assert(A <> B). intro. subst B. apply H3. Col. split. assumption. split. induction(eq_dec_points A X). treat_equalities. exists B. split. Col. intro. apply H3. eapply col3. apply H. Col. Col. Col. exists A. split. Col. intro. apply H3. assert(Col A P X). eapply col3. apply H. Col. Col. Col. ColR. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles