proposition: Lemma inter_right_comm : forall A B C D X, Inter A B C D X -> Inter A B D C X.
proof: Proof. intros. unfold Inter in *. spliter. ex_and H0 P. split. auto. split. exists P. split. Col. assumption. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles