proposition: Lemma halfa_chara1 : forall P A O B, HalfA 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.
proof: Proof. unfold HalfA. intros P A O B H. spliter. assert_diffs. destruct (l6_11_existence O O A B) as [A' []]; auto. destruct (midpoint_existence A A') as [M]. exists A', M. split. assumption. split. assumption. split. assumption. destruct (col_dec A O B) as [|HNCol]. { assert (Out O A B). apply not_bet_out; assumption. assert (A = A') by (apply (l6_11_uniqueness O O A B); Cong). treat_equalities. apply in_angle_out with B; trivial. } assert (InAngle M A O B). { assert_diffs. assert (O <> M). { intro. subst M. absurd (Bet A O B); trivial. apply between_symmetry, l6_2 with A'; Between. } apply l11_25 with M A A'; [|apply out_trivial|apply l6_6|apply out_trivial]; auto. repeat split; auto. exists M. split; Between. right. apply out_trivial; auto. } apply col_inangle2__out with A B; trivial. apply conga2_cop2__col_1 with A B; [| |apply conga_comm; assumption|Cop..]. intro; destruct (or_bet_out A O B) as [|[|]]; auto. assert_diffs. destruct (l11_51 O M A O M A'); Cong. intro; treat_equalities; apply HNCol; Col. apply l11_10 with M A M A'; [|apply out_trivial..|apply l6_6]; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma