proposition: Lemma proj_distinct : forall P P' A B, Projp P P' A B -> P' <> A \/ P' <> B.
proof: Proof. intros. unfold Projp in H. spliter. induction H0. spliter. induction(eq_dec_points P' A). subst P'. right. apply perp_not_eq_1 in H1. assumption. left. assumption. spliter. subst P'. induction(eq_dec_points P A). subst P. right. assumption. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors