proposition: Lemma one_side_reflexivity : forall P Q A, ~ Col A P Q -> OS P Q A A.
proof: Proof. intros. unfold OS. double A P C. exists C. assert (TS P Q A C). repeat split. assumption. intro. apply H. apply col_permutation_2. eapply (col_transitivity_1 _ C). intro. subst C. apply l7_2 in H0. apply is_midpoint_id in H0. subst A. apply H. assumption. apply col_permutation_4. assumption. unfold Col. right; right. apply midpoint_bet. assumption. exists P. split. apply col_trivial_1. apply midpoint_bet. assumption. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar