proposition: Lemma null_halfa__null : forall P A O B, Col A O B -> HalfA P A O B -> Out O A P.
proof: Proof. unfold HalfA. intros P A O B HCol H. spliter. assert (Out O A B) by (apply not_bet_out; assumption). apply(in_angle_out A O B P); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma