proposition: Lemma halfa__ts : forall P A O B, ~ Col A O B -> HalfA P A O B -> TS O P A B.
proof: Proof. intros P A O B HNCol HHalfa. assert(~ Col A O P) by (apply halfa_not_null with B; assumption). assert(~ Col B O P). apply halfa_not_null with A; Col. apply halfa_sym; assumption. destruct HHalfa as [_ []]. apply invert_two_sides, in_angle_two_sides; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma