proposition: Lemma eqv_project_eq_eq : forall P Q R S P' Q' 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 P' A B X Y -> Proj S S' A B X Y -> Q' = S'.
proof: Proof. intros. spliter. induction(eq_dec_points P Q). subst Q. apply null_vector in H. subst S. assert(Q' = P'). eapply project_uniqueness. apply H1. assumption. subst Q'. eapply project_uniqueness. apply H2. assumption. assert(R <> S). intro. subst S. apply H4. eapply null_vector. apply eqv_sym in H. apply H. assert(EqV P R Q S). apply eqv_permut. assumption. induction(eq_dec_points P R). subst R. apply null_vector in H6. subst S. eapply project_uniqueness. apply H1. assumption. assert( Q <> S). intro. subst S. apply eqv_sym in H6. apply null_vector in H6. contradiction. eapply project_par. apply H1. apply H3. eapply par_trans. apply par_symmetry. apply eqv_par in H6; auto. apply H6. unfold Proj in H0. unfold Proj in H2. spliter. induction H16; induction H12. assert(Col R P P' /\ Col P' P P'). apply(parallel_uniqueness X Y P P' R P' P'); Col. Par. Par. spliter. clear H18. eapply (par_col_par_2 _ P'); Col. subst P'. assumption. subst P'. Par. subst P'. subst R. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors