proposition: Lemma inter_trivial : forall A B X, ~ Col A B X -> Inter A X B X X.
proof: Proof. intros. assert_diffs. unfold Inter. repeat split; Col. exists B. split. Col. intro. apply H. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles