proposition: Lemma l14_36_a : forall O E E' A B C, Sum O E E' A B C -> Out O A B -> Bet O A C.
proof: Proof. intros. assert(HS:=H). unfold Sum in H. spliter. unfold Ar2 in H. unfold Out in H0. spliter. assert(Parallelogram_flat O A C B). apply(sum_cong O E E' H A B C HS). tauto. assert(Parallelogram O A C B). right. auto. induction(eq_dec_points A B). subst B. unfold Parallelogram_flat in H7. spliter. assert(O = C \/ Midpoint A O C). apply(l7_20 A O C); Cong. induction H13. subst C. apply False_ind. apply HS. apply (double_null_null O E E') in HS; auto. tauto. unfold Midpoint in H13. tauto. induction H3. apply plg_permut in H8. apply plg_permut in H8. apply plg_permut in H8. assert(Bet A B C). apply between_symmetry. apply(plg_bet1 B O A C). assumption. apply between_symmetry. assumption. apply (outer_transitivity_between O A B C); auto. assert(Bet B A C). apply between_symmetry. apply(plg_bet1 A O B C). apply plg_comm2. assumption. apply between_symmetry. assumption. apply (outer_transitivity_between2 O B A C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod