proposition: Lemma symmetry_preserves_one_side : forall A B X Y M A' B', Col X Y M -> OS X Y A B -> Midpoint M A A' -> Midpoint M B B' -> OS X Y A' B'.
proof: Proof. intros. assert(X <> Y /\ ~Col A X Y /\ ~Col B X Y). unfold OS in H0. ex_and H0 P. unfold TS in H0. unfold TS in H3. spliter. repeat split; auto. intro. subst Y. Col. spliter. assert(A <> M). intro. subst M. apply H4. Col. assert(A' <> M). intro. subst M. apply H6. apply sym_equal. apply is_midpoint_id. apply l7_2. assumption. assert(B <> M). intro. subst M. apply H5. Col. assert(B' <> M). intro. subst M. apply H8. apply sym_equal. apply is_midpoint_id. apply l7_2. assumption. assert(TS X Y A A'). unfold TS. repeat split; auto. intro. apply H4. unfold Midpoint in H1. spliter. apply bet_col in H1. assert(Col M A' X). ColR. assert(Col M A' Y). ColR. eapply (col3 A' M); Col. exists M. split. Col. apply midpoint_bet. assumption. assert(TS X Y B B'). unfold TS. repeat split; auto. intro. apply H5. unfold Midpoint in H2. spliter. apply bet_col in H2. assert(Col M B' X). ColR. assert(Col M B' Y). ColR. eapply (col3 B' M); Col. exists M. split. Col. apply midpoint_bet. assumption. eapply l9_8_1. apply l9_2. apply H10. apply l9_2. eapply l9_8_2. apply H11. apply one_side_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel