proposition: Lemma project_preserves_eqv : forall P Q R S P' Q' R' S' A B X Y, EqV P Q R S -> Proj P P' A B X Y -> Proj Q Q' A B X Y -> Proj R R' A B X Y -> Proj S S' A B X Y -> EqV P' Q' R' S'.
proof: Proof. intros. induction (eq_dec_points P Q). subst Q. apply null_vector in H. subst S. assert(R'=S'). eapply project_uniqueness. apply H2. apply H3. subst S'. assert(P' = Q'). eapply project_uniqueness. apply H0. apply H1. subst Q'. apply eqv_trivial. assert(R <> S). intro. subst S. apply eqv_sym in H. apply null_vector in H. contradiction. induction (par_dec P Q A B). assert(EqV P Q P' Q'). eapply project_par_eqv. apply H0. assumption. assumption. assert(EqV R S R' S'). eapply project_par_eqv. apply H2. assumption. eapply par_trans. apply par_symmetry. apply eqv_par. apply H4. assumption. assumption. eapply eqv_trans. apply eqv_sym. apply H7. eapply eqv_trans. apply H. assumption. induction (par_dec P Q X Y). assert(P' = Q'). eapply project_par. apply H0. apply H1. assumption. assert(Par R S X Y). apply eqv_par in H; auto. eapply par_trans. apply par_symmetry. apply H. assumption. assert(R' = S'). eapply project_par. apply H2. apply H3. assumption. subst Q'. subst S'. apply eqv_trivial. assert(P' <> Q'). intro. subst Q'. apply H7. eapply (ker_par P Q P' A B); auto. assert(~ Par R S X Y). intro. apply H7. apply eqv_par in H; auto. eapply par_trans. apply H. assumption. assert(R' <> S'). intro. subst S'. apply H9. eapply (ker_par R S R' A B); auto. assert(HH1:= vector_construction P Q P'). ex_and HH1 Q''. assert(HH1:= vector_construction R S R'). ex_and HH1 S''. assert(EqV P' Q'' R' S''). eapply eqv_trans. apply eqv_sym. apply H11. eapply eqv_trans. apply H. assumption. assert(Q' <> Q''). intro. apply H6. subst Q''. apply eqv_par in H; auto. apply eqv_par in H11; auto. apply eqv_par in H12; auto. assert(P' <> Q'). intro. subst Q'. apply par_distincts in H11. tauto. apply eqv_par in H13; auto. assert(Par P' Q' A B). right. unfold Proj in *. spliter. repeat split; Col. eapply par_trans. apply H. eapply par_trans. apply H12. eapply par_trans. apply par_symmetry. apply H13. assumption. assert(S' <> S''). intro. subst S''. apply eqv_par in H; auto. apply eqv_par in H11; auto. apply eqv_par in H12; auto. assert(R' <> S'). intro. subst S'. apply par_distincts in H12. tauto. apply eqv_par in H13; auto. assert(Par R' S' A B). right. unfold Proj in *. spliter. repeat split; Col. apply H6. eapply par_trans. apply H. eapply par_trans. apply H12. assumption. intro. subst Q''. apply null_vector in H13. subst S'. tauto. assert(HP1:=eqv_permut P Q P' Q'' H11). assert(HP2:=eqv_permut R S R' S'' H12). assert(HP3:=eqv_permut P' Q'' R' S'' H13). assert(Proj Q'' Q' A B X Y). eapply eqv_eq_project. apply H11. apply H0. assumption. eapply project_idem. apply H0. assert(Proj S'' S' A B X Y). eapply eqv_eq_project. apply H12. apply H2. assumption. eapply project_idem. apply H2. assert(HH1:= H16). assert(HH2:= H17). eapply project_par_dir in HH1; auto. apply project_par_dir in HH2; auto. assert(Par Q'' Q' S'' S'). eapply par_trans. apply HH1. Par. assert(~ Col A B Q''). apply(project_not_col A B X Y Q'' Q' H16). auto. assert(~ Col P' Q'' Q'). intro. apply H19. unfold Proj in *. spliter. assert(Col P' Q' A). ColR. assert(Col P' Q' B). ColR. apply (col3 P' Q'); Col. assert(Cong_3 P' Q'' Q' R' S'' S'). eapply cong_conga3_cong3. assumption. apply eqv_cong. assumption. eapply par3_conga3. assumption. apply eqv_par. intro. subst Q''. apply H20. Col. assumption. assumption. right. unfold Proj in *. spliter. repeat split; try assumption. apply (col3 A B); Col. apply (col3 A B); Col. assert(EqV Q'' Q' S'' S'). unfold EqV. left. induction(eq_dec_points Q' S'). subst S'. assert(P' = R'). apply (eqv_project_eq_eq Q'' P' S'' R' Q' P' R' A B X Y); auto. apply eqv_comm. assumption. eapply project_idem. apply H0. eapply project_idem. apply H2. subst R'. apply null_vector in HP3. subst S''. apply plg_trivial. auto. induction(eq_dec_points P' R'). subst R'. apply null_vector in HP3. subst S''. assert(Q' = S'). eapply eqv_project_eq_eq; [apply H13| |apply H16|..]. eapply project_idem. apply H0. eapply project_idem. apply H0. assumption. subst S'. apply plg_trivial. auto. apply plg_to_parallelogram. unfold Plg. split. left. intro. subst Q''. apply H19. unfold Proj in *. spliter. Col. eapply par_cong_mid_os. induction H18. assumption. spliter. apply False_ind. assert(~ Col A B S''). apply(project_not_col A B X Y S'' S' H17). auto. apply H27. unfold Proj in *. spliter. assert(Col Q' S' A). ColR. assert(Col Q' S' B). ColR. apply (col3 Q' S'); Col. unfold Cong_3 in H21. spliter. Cong. unfold EqV in H13. induction H13. apply plg_permut in H13. assert(Parallelogram_strict R' P' Q'' S''). apply plg_sym in H13. induction H13. assumption. unfold Parallelogram_flat in H13. spliter. apply False_ind. apply H19. unfold Proj in *. spliter. assert(Col P' R' A). ColR. assert(Col P' R' B). ColR. apply (col3 P' R'); Col. assert(HH:= plgs_par_strict R' P' Q'' S'' H24). spliter. assert(Par_strict Q'' S'' Q' S'). eapply par_strict_col2_par_strict. auto. apply par_strict_symmetry. apply H25. unfold Proj in *. spliter. apply (col3 A B); Col. unfold Proj in *. spliter. apply (col3 A B); Col. apply l12_6. assumption. spliter. subst Q''. apply False_ind. apply H20. Col. eapply eqv_sum. apply H13. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors