proposition: Lemma project_to_projp : forall P P' A B X Y, Proj P P' A B X Y -> Perp A B X Y -> Projp P P' A B.
proof: Proof. intros. unfold Proj in H. spliter. unfold Projp. split. apply perp_not_eq_1 in H0. assumption. induction H4. left. split. assumption. apply perp_sym. eapply par_perp__perp. apply par_symmetry. apply H4. Perp. right. subst P'. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors