proposition: Lemma l11_19 : forall A B P1 P2, Per A B P1 -> Per A B P2 -> OS A B P1 P2 -> Out B P1 P2.
proof: Proof. intros. induction (col_dec A B P1). induction (l8_9 A B P1 H H2). subst. unfold OS in *. decompose [ex and] H1. unfold TS in *. intuition. subst. unfold OS in *. decompose [ex and] H1. unfold TS in *. spliter. assert (Col B A B) by Col. intuition. induction (col_dec A B P2). induction (l8_9 A B P2 H0 ). subst. unfold OS in *. decompose [ex and] H1. unfold TS in *. intuition. subst. unfold OS in *. decompose [ex and] H1. unfold TS in *. spliter. assert (Col B A B) by Col. intuition. Col. assert (T:=l11_15 A B P1 A B P2 H2 H3). decompose [ex and] T. apply H7. split. split. apply conga_refl. intro;subst;Col. intro;subst;Col. apply invert_one_side;auto. split. apply l11_16;try assumption. intro;subst;Col. intro;subst;Col. intro;subst;Col. intro;subst;Col. apply one_side_reflexivity. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2