proposition: Lemma prod_uniquenessB : forall O E E' A B B' C, A <> O -> Prod O E E' A B C -> Prod O E E' A B' C -> B = B'.
proof: Proof. intros. apply prod_comm in H0. apply prod_comm in H1. apply (prod_uniquenessA O E E' B B' A C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum