proposition: Lemma cop_halfa_perp__os : forall P A O B T, HalfA P A O B -> Perp O P T O -> Coplanar A O P T -> OS O T P A.
proof: Proof. intros P A O B T HP HPerp HCop. apply acute_cop_perp__one_side. apply acute_sym, halfa__acute with B; assumption. assumption. Cop. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma