proposition: Lemma perp_projp : forall P P' A B, Perp_at P' A B P P' -> Projp P P' A B.
proof: Proof. intros. unfold Projp. split. apply l8_14_2_1a in H. apply perp_not_eq_1 in H. assumption. left. split. apply perp_in_col in H. spliter. assumption. apply l8_14_2_1a in H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors