proposition: Lemma projp_id : forall P P' Q' A B, Projp P P' A B -> Projp P Q' A B -> P' = Q'.
proof: Proof. intros. unfold Projp in *. spliter. induction H1; induction H2. spliter. apply (l8_18_uniqueness A B P); Col. apply perp_not_col2 in H4. induction H4. assumption. contradiction. spliter. subst P'. apply perp_not_col2 in H3. induction H3; contradiction. spliter. subst Q'. apply perp_not_col2 in H4. induction H4; contradiction. spliter. subst P'. subst Q'. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors