proposition: Lemma same_dir_trans : forall A B C D E F, Same_dir A B C D -> Same_dir C D E F -> Same_dir A B E F.
proof: Proof. intros. unfold Same_dir in *. induction H; induction H0; spliter. left. tauto. ex_and H0 F'. subst B. subst D. apply null_vector in H2. subst F'. unfold Out in H0. tauto. ex_and H D'. subst D. subst F. unfold Out in H. tauto. ex_and H D'. ex_and H0 F'. right. induction(eq_dec_points A B). subst B. apply null_vector in H1. subst D'. unfold Out in H. tauto. assert(HH:=vector_construction A B E). ex_and HH F''. exists F''. split; trivial. assert(C <> D /\ C <> D' /\ E <> F /\ E <> F'). unfold Out in *. spliter. repeat split; auto. spliter. unfold EqV in *. induction H1; induction H2; induction H4. unfold Out in *. spliter. induction H10; induction H12. repeat split. auto. intro. subst F''. induction H4. apply H4. Col. apply plgf_sym in H4. apply plgf_trivial_neq in H4. tauto. left. assert(Bet E F' F''). apply (plg_plg_bet C D _ _ D'). apply H2. apply H12. assert(Parallelogram C D' F'' E \/ C = D' /\ B = A /\ E = F'' /\ C = E). apply(plg_pseudo_trans C D' B A E F''). apply plg_sym. apply plg_comm2. auto. apply plg_comm2. auto. induction H13. assumption. tauto. apply (between_exchange4 _ _ F'). apply H10. auto. repeat split. auto. intro. subst F''. induction H4. apply H4. Col. apply plgf_sym in H4. apply plgf_trivial_neq in H4. tauto. assert(Bet E F'' F'). apply (plg_plg_bet C D' _ _ D); trivial. assert(Parallelogram C D' F'' E \/ C = D' /\ B = A /\ E = F'' /\ C = E). apply plg_pseudo_trans. apply plg_sym. apply plg_comm2. auto. apply plg_comm2. auto. induction H13. assumption. tauto. apply (l5_3 _ _ _ F'). apply H10. assumption. repeat split. auto. intro. subst F''. induction H4. apply H4. Col. apply plgf_sym in H4. apply plgf_trivial_neq in H4. tauto. assert(Bet E F' F''). apply (plg_plg_bet C D _ _ D'). apply H2. apply H12. assert(Parallelogram C D' F'' E \/ C = D' /\ B = A /\ E = F'' /\ C = E). apply plg_pseudo_trans. apply plg_sym. apply plg_comm2. auto. apply plg_comm2. auto. induction H13. assumption. tauto. apply (l5_1 _ F'). apply H8. auto. auto. repeat split. auto. intro. subst F''. induction H4. apply H4. Col. apply plgf_sym in H4. apply plgf_trivial_neq in H4. tauto. assert(Bet E F'' F'). apply (plg_plg_bet C D' _ _ D); trivial. assert(Parallelogram C D' F'' E \/ C = D' /\ B = A /\ E = F'' /\ C = E). apply plg_pseudo_trans. apply plg_sym. apply plg_comm2. auto. apply plg_comm2. auto. induction H13. auto. tauto. right. apply (between_exchange4 _ _ F'). apply H13. auto. tauto. tauto. tauto. tauto. tauto. tauto. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec