proposition: Lemma prod_uniqueness : forall A B C1 C2, Prod O E E' A B C1 -> Prod O E E' A B C2 -> C1 = C2.
proof: Proof. intros. apply prod_to_prodp in H. apply prod_to_prodp in H0. unfold Prodp in *. spliter. ex_and H4 B'. ex_and H2 B''. assert(B'=B''). eapply (project_uniqueness B B' B'' O E' E E'); auto; unfold Prod in H. subst B''. eapply (project_uniqueness B' C1 C2 O E A E'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum