proposition: Lemma out_out_one_side : forall A B X Y Z, OS A B X Y -> Out A Y Z -> OS A B X Z.
proof: Proof. intros. assert (A <> B). unfold OS in H. ex_and H C. unfold TS in H. spliter. intro. subst B. Col. prolong Y A Y' A Y. assert(OS A B Y Z). unfold OS. exists Y'. split. unfold TS. repeat split. apply one_side_symmetry in H. eapply one_side_not_col123 in H. intro. apply H. apply col_permutation_1. assumption. intro. apply one_side_symmetry in H. eapply one_side_not_col123 in H. apply H. assert(Col A B Y). eapply (col_transitivity_1 _ Y'). intro. subst Y'. apply cong_symmetry in H3. apply cong_identity in H3. subst Y. unfold Out in H0. spliter. absurde. apply col_permutation_4. assumption. unfold Col. right; right. assumption. assumption. exists A. split. apply col_trivial_1. assumption. unfold TS. repeat split. intro. apply one_side_symmetry in H. eapply one_side_not_col123 in H. apply H. eapply (col_transitivity_1 _ Z). intro. subst Z. unfold Out in H0. spliter. absurde. apply col_permutation_4. assumption. apply out_col in H0. apply col_permutation_5. assumption. apply one_side_symmetry in H. eapply one_side_not_col123 in H. intro. apply H. eapply (col_transitivity_1 _ Y'). intro. subst Y'. apply cong_symmetry in H3. apply cong_identity in H3. subst Y. apply H. apply col_trivial_3. apply col_permutation_4. assumption. unfold Col. right; right. assumption. exists A. split. apply col_trivial_1. unfold Out in H0. spliter. induction H5. apply between_symmetry. eapply outer_transitivity_between. apply between_symmetry. apply H2. assumption. auto. apply between_symmetry. eapply between_inner_transitivity. apply between_symmetry. apply H2; spliter. assumption. eapply one_side_transitivity. apply H. apply H4. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar