proposition: Lemma projp_to_project : forall P P' A B X Y, Perp A B X Y -> Projp P P' A B -> Proj P P' A B X Y.
proof: Proof. intros. unfold Proj. repeat split. eapply perp_not_eq_1. apply H. eapply perp_not_eq_2. apply H. apply perp_not_par. assumption. unfold Projp in H0. spliter. induction H1. spliter. assumption. spliter. subst P'. assumption. unfold Projp in H0. spliter. induction H1. spliter. left. eapply l12_9_2D. apply perp_sym. apply H2. Perp. spliter. right. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors