proposition: Lemma project_uniqueness : forall P P' Q' A B X Y, Proj P P' A B X Y -> Proj P Q' A B X Y -> P' = Q'.
proof: Proof. intros. assert(HH:=H). assert(HH0:=H0). unfold Proj in HH. unfold Proj in HH0. spliter. clean_duplicated_hyps. induction H10; induction H5. apply par_distincts in H1. apply par_distincts in H2. spliter. clear H5. assert(Col P P P' /\ Col Q' P P'). apply(parallel_uniqueness X Y P P' P Q' P); Col. Par. Par. spliter. clear H3. apply (l6_21 A B P P'); Col. intro. apply H10. eapply project_id. apply H. Col. subst Q'. apply sym_equal. eapply project_id. apply H. Col. subst P'. eapply project_id. apply H0. Col. subst P'. subst Q'. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors