proposition: Lemma halfa_chara2 : forall P A O B, (exists A', exists M, Cong O A' O A /\ Out O A' B /\ Midpoint M A A' /\ Out O M P) -> HalfA P A O B.
proof: Proof. intros P A O B H. destruct H as [A' [M [HCong [HOut [HM1 HM2]]]]]. assert_diffs. apply out_preserves_halfa with M A A'; trivial. apply out_trivial; auto. split; [|split]. - intro. absurd (O = M); auto. apply l7_17 with A A'; trivial. split; Cong. - repeat split; auto. exists M. split. Between. right; apply out_trivial; auto. - destruct (eq_dec_points A A'). subst; apply conga_refl; auto. assert_diffs. destruct (l11_51 O A M O A' M); Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma