proposition: Lemma prod_comm : forall O E E' A B C, Prod O E E' A B C -> Prod O E E' B A C.
proof: Proof. intros. assert(Ar2 O E E' A B C). unfold Prod in H. tauto. unfold Ar2 in H0. spliter. induction(eq_dec_points A O). subst A. assert(HH:=prod_0_l O E E' B H0 H2). assert(C = O). apply(prod_uniqueness O E E' O B); auto. subst C. eapply (prod_0_r O E E'); Col. induction(eq_dec_points B O). subst B. assert(HH:=prod_0_r O E E' A H0 H1). assert(C = O). apply(prod_uniqueness O E E' A O); auto. subst C. apply (prod_0_l O E E'); Col. induction(eq_dec_points C O). subst C. apply prod_null in H. induction H; contradiction. unfold Prod in *. repeat split; auto. spliter. ex_and H7 B'. assert(HG:=grid_not_par O E E' H0). spliter. assert(exists ! P' : Tpoint, Proj A P' O E' E E'). apply(project_existence A O E' E E'); Col. intro. apply H12. Par. ex_and H16 A'. unfold unique in H17. spliter. clear H17. unfold Proj in H16. spliter. clean_duplicated_hyps. assert(Par A A' E E'). induction H20. Par. subst A'. apply False_ind. apply H0. ColR. clear H20. exists A'. repeat split. left. Par. Col. left. apply par_comm. apply par_symmetry. apply (l13_11 C B A E' A' B' O); Col. intro. apply H0. ColR. ColR. ColR. intro. subst A'. apply H10. apply par_symmetry. apply(par_col_par _ _ _ A); Par; Col. induction H7. intro. subst B'. apply H10. apply par_symmetry. apply(par_col_par _ _ _ B); Par; Col. subst B'. intro. contradiction. ColR. induction H7. apply(par_trans _ _ E E'); Par. subst B'. apply False_ind. apply H0. ColR. induction H9. Par. subst B'. apply False_ind. apply H0. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum