proposition: Lemma acute_cop_perp__one_side : forall P A O B, Acute A O P -> Perp O A B O -> Coplanar A B O P -> OS O B A P.
proof: Proof. intros. induction(col_dec A O P). apply(acute_one_side_aux0); auto. assert(~Col A O B). { apply perp_not_col in H0. Col. } assert(TS O A P B \/ OS O A P B). { apply(cop__one_or_two_sides O A P B); Col. Cop. } induction H4. assert(HC:=symmetric_point_construction B O). ex_and HC Bs. unfold Midpoint in *. spliter. assert(TS O A Bs B). { repeat split; Col. intro. apply H3. ColR. exists O. split; [Col|Between]. } assert(OS O A P Bs). { apply(l9_8_1 _ _ _ _ B); auto. } assert(Perp O A Bs O ). { apply perp_sym. apply perp_comm. apply (perp_col _ B); Perp. intro. treat_equalities. apply H3; Col. Col. } assert(OS O Bs A P). { apply(acute_one_side_aux P A O Bs); auto. } apply(col_one_side _ Bs); Col. intro. treat_equalities. apply H3; Col. apply(acute_one_side_aux P A O B); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2