proposition: Lemma projp_project_to_perp : forall P P' A B X Y, P <> P' -> Projp P P' A B -> Proj P P' A B X Y -> Perp A B X Y.
proof: Proof. intros. unfold Projp in H0. unfold Proj in H1. spliter. induction H6; induction H5. spliter. apply perp_sym. eapply par_perp__perp. apply H5. Perp. contradiction. spliter. contradiction. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors