proposition: Lemma project_existence : forall P A B X Y, X<>Y -> A<>B -> ~ Par X Y A B -> exists! P', Proj P P' A B X Y.
proof: Proof. intros. assert (T:=parallel_existence X Y P H). decompose [ex and] T;clear T. assert (~ Par x x0 A B) by ( intro; assert (Par X Y A B) by ( eapply par_trans;eauto; intuition); intuition). apply (not_par_inter_exists x x0 A B) in H4. DecompExAnd H4 P'. exists P'. unfold unique. assert (Proj P P' A B X Y). unfold Proj. repeat split. assumption. assumption. intro. Par. Col. induction (eq_dec_points P P'). tauto. left. apply par_symmetry. apply par_col2_par with x x0;Col. split. assumption. intros. eapply project_uniqueness;eauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors