proposition: Lemma inv_exists : forall O E E' A, ~ Col O E E' -> Col O E A -> A <> O -> exists IA, Prod O E E' IA A E.
proof: Proof. intros. unfold Prod. repeat split; Col. assert(HH:=(grid_not_par O E E' H)). spliter. assert(exists ! P' : Tpoint, Proj A P' O E' E E'). apply(project_existence A O E' E E' H7 H6). intro. apply H4. Par. ex_and H8 B'. unfold unique in H9. spliter. clear H9. unfold Proj in H8. spliter. assert(B' <> O). intro. subst B'. induction H12. induction H12. apply H12. exists E. split; Col. spliter. contradiction. contradiction. assert(exists ! P' : Tpoint, Proj E' P' O E B' E). apply(project_existence E' O E B' E); auto. intro. subst B'. apply H. Col. intro. induction H14. apply H14. exists E. split; Col. spliter. apply H. ColR. ex_and H14 IA. unfold unique in H15. spliter. clear H15. unfold Proj in H14. spliter. exists IA. repeat split; Col. exists B'. assert(Par A B' E E'). induction H12. Par. subst B'. apply False_ind. apply H16. right. repeat split; Col. clear H12. repeat split. left. Par. Col. induction H18. left. Par. subst IA. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum