proposition: Lemma prod_uniquenessA : forall O E E' A A' B C, B <> O -> Prod O E E' A B C -> Prod O E E' A' B C -> A = A'.
proof: Proof. intros. assert(HP1:= H0). assert(HP2:= H1). unfold Prod in H0. unfold Prod in H1. spliter. unfold Ar2 in *. spliter. clean_duplicated_hyps. induction(eq_dec_points A' O). subst A'. assert(C = O). assert(HH:= prod_0_l O E E' B H0 H8). apply(prod_uniqueness O E E' O B); auto. subst C. apply prod_null in HP1. induction HP1. assumption. contradiction. ex_and H3 B'. ex_and H2 B''. assert(B' = B''). induction H3; induction H2. assert(Par B B' B B''). apply (par_trans _ _ E E'); Par. induction H12. apply False_ind. apply H12. exists B. split; Col. spliter. apply(l6_21 O E' B B'); Col. intro. apply H0. ColR. subst B''. apply False_ind. apply H0. ColR. subst B'. apply False_ind. apply H0. ColR. subst B. assumption. subst B''. assert(HH:= grid_not_par O E E' H0). spliter. induction H6; induction H11. assert(Par E' A' E' A). apply(par_trans _ _ B' C); Par. induction H18. apply False_ind. apply H18. exists E'. split; Col. spliter. apply(l6_21 O E E' A); Col. subst B'. apply par_distincts in H6. tauto. subst B'. apply par_distincts in H11. tauto. subst B'. induction(eq_dec_points C O). subst C. apply prod_null in HP1. apply prod_null in HP2. induction HP1; induction HP2; try contradiction. apply False_ind. apply H0. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum