proposition: Lemma eqv_eq_project : forall P Q R S P' Q' 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 Q' A B X Y.
proof: Proof. intros. assert(HH1:=H1). unfold Proj in HH1. spliter. repeat split; Col. apply eqv_permut in H. induction(eq_dec_points S Q'). right. assumption. left. induction(eq_dec_points P R). subst R. apply null_vector in H. subst S. unfold Proj in H1. spliter. induction H11. assumption. contradiction. apply eqv_par in H; auto. assert(Col P R P'). eapply ker_col. apply H0. assumption. unfold Proj in H0. spliter. induction H14. assert(Par P R X Y). apply (par_col_par_2 _ P'); Col. induction H7. assert(Col Q Q Q' /\ Col S Q Q'). apply(parallel_uniqueness X Y Q Q' Q S Q); Col. Par. eapply par_trans; [|apply H]. Par. spliter. apply par_left_comm. eapply (par_col_par_2 _ Q); Col. Par. subst Q'. eapply par_trans. apply par_left_comm. apply par_symmetry. apply H. assumption. subst P'. assert(Par P R X Y). unfold Proj in H2. spliter. induction H17. Par. subst R. tauto. induction H7. assert(Col Q Q Q' /\ Col S Q Q'). apply(parallel_uniqueness X Y Q Q' Q S Q); Col. Par. eapply par_trans. apply par_symmetry. apply H14. assumption. spliter. apply (par_col_par_2 _ Q); Col. eapply par_trans. apply par_left_comm. apply par_symmetry. apply H. assumption. subst Q'. eapply par_trans. apply par_symmetry. apply par_right_comm. apply H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors