proposition: Lemma project_par : forall A B X Y P Q P' Q', Proj P P' A B X Y -> Proj Q Q' A B X Y -> Par P Q X Y -> P' = Q'.
proof: Proof. intros. assert(HH:=H). assert(HH0:=H0). unfold Proj in HH. unfold Proj in HH0. spliter. apply par_distincts in H1. spliter. induction H11. assert(Col P P P' /\ Col Q P P'). apply(parallel_uniqueness X Y P P' P Q P); Col. Par. Par. spliter. apply par_distincts in H11. spliter. induction H6. assert(Col P Q Q' /\ Col Q Q Q'). apply(parallel_uniqueness X Y Q Q' P Q Q); Col. Par. Par. spliter. clean_duplicated_hyps. clear H14. clear H19. apply par_distincts in H6. spliter. eapply (l6_21 A B P Q); Col. intro. apply H16. apply(project_id A B X Y P P'); Col. subst Q'. eapply (l6_21 A B P Q); Col. intro. apply H16. apply(project_id A B X Y P P'); Col. induction H6. apply par_distincts in H6. spliter. assert(Col P Q Q' /\ Col Q Q Q'). apply(parallel_uniqueness X Y Q Q' P Q Q); Col. Par. Par. spliter. clear H17. subst P'. eapply (l6_21 A B Q P); Col. intro. apply H14. apply(project_id A B X Y Q Q'); Col. subst P'. subst Q'. apply False_ind. apply H4. induction(eq_dec_points A P). subst P. eapply (par_col_par_2 _ Q); Col. eapply (par_col_par_2 _ P); Col. apply par_left_comm. eapply (par_col_par_2 _ Q); Col. ColR. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors