proposition: Lemma projp_preserves_eqv : forall A B C A' B' C' D D' X Y, EqV A B C D -> Projp A A' X Y -> Projp B B' X Y -> Projp C C' X Y -> Projp D D' X Y -> EqV A' B' C' D'.
proof: Proof. intros. eapply projp_is_project_perp in H0. ex_and H0 T. ex_and H4 U. eapply (project_preserves_eqv A B C D A' B' C' D' X Y T U). apply H. assumption. eapply projp_to_project in H1. apply H1. auto. eapply projp_to_project in H2. apply H2. auto. eapply projp_to_project in H3. apply H3. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors