proposition: Lemma par_one_or_two_sides : forall A B C D, Par_strict A B C D -> TS A C B D /\ TS B D A C \/ OS A C B D /\ OS B D A C.
proof: Proof. intros. induction(two_sides_dec A C B D). left. split. assumption. apply par_two_sides_two_sides. apply par_comm. unfold Par. left. assumption. assumption. right. assert(HH:=H). unfold Par_strict in H. spliter. split. apply cop_nts__os; Cop. intro. apply H1. exists C. split; Col. intro. apply H1. exists A. split; Col. apply cop_nts__os; Cop. intro. apply H1. exists D. split; Col. intro. apply H1. exists B. split; Col. intro. apply H0. apply par_two_sides_two_sides. left. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles