proposition: Lemma bet_same_dir2 : forall A B C, A <> B -> B <> C -> Bet A B C -> Same_dir A B B C.
proof: Proof. intros. unfold Same_dir. right. assert(HH:=vector_construction A B B). ex_and HH C'. exists C'. split; trivial. unfold EqV in H2. induction H2; [|tauto]. induction H2. apply plgs_par_strict in H2. spliter. apply False_ind. apply H3. exists B. split; Col. assert(HH:= H2). unfold Parallelogram_flat in HH. apply plgf_bet in H2. spliter. unfold Out. repeat split. auto. intro. subst C'. apply cong_identity in H5. contradiction. induction H2. assert(Bet B A B). spliter. apply (outer_transitivity_between2 _ C'). Between. auto. induction H7. auto. tauto. apply between_identity in H8. subst B. tauto. induction H2. assert(Bet B A B). spliter. apply (outer_transitivity_between _ _ C'). apply H2. auto. induction H7. auto. tauto. apply between_identity in H8. subst B. tauto. induction H2. assert( A = C' \/ Midpoint B A C'). apply l7_20. Col. Cong. induction H8. induction H7. tauto. tauto. unfold Midpoint in H8. spliter. apply (l5_2 A); auto. assert( A = C' \/ Midpoint B A C'). apply l7_20. Col. Cong. induction H8. induction H7. tauto. tauto. unfold Midpoint in H8. spliter. apply (l5_2 A); auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec