proposition: Lemma cop_halfa_perp__os2 : 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 /\ OS O T P B.
proof: Proof. intros P A O B T HP HPerp HCop. split. apply cop_halfa_perp__os with B; assumption. apply cop_halfa_perp__os with A. apply halfa_sym; assumption. assumption. destruct (col_dec A O P). { assert (Col B O P); [|Cop]. destruct HP as [_ []]. apply (col_conga_col A O P); assumption. } apply halfa__coplanar in HP. apply coplanar_perm_12, coplanar_trans_1 with A; Cop. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma