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