proposition: Lemma projp_is_project : forall P P' A B, Projp P P' A B -> exists X, exists Y, Proj P P' A B X Y.
proof: Proof. intros. assert(A <> B). unfold Projp in H. tauto. assert(HH:=perp_vector A B H0). ex_and HH X. ex_and H1 Y. exists X. exists Y. assert(X <> Y). apply perp_not_eq_2 in H2. assumption. unfold Proj. repeat split; auto. apply perp_not_par. assumption. unfold Projp in H. spliter. induction H3. tauto. spliter. subst P'. assumption. unfold Projp in H. spliter. induction H3. spliter. left. eapply l12_9_2D. apply perp_sym. apply H4. Perp. right. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors