proposition: Lemma par_strict_irreflexivity : forall A B, ~ Par_strict A B A B.
proof: Proof. intros. intro. unfold Par_strict in H. spliter. apply H0. exists A. split; apply col_trivial_1. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles