proposition: Lemma prod_1_l_eq : forall O E E' A B, Prod O E E' A B B -> A = E \/ B = O.
proof: Proof. intros. assert(HP:=H). unfold Prod in H. spliter. unfold Ar2 in H. spliter. clear H0. assert(HH:= prod_1_l O E E' B H H2). induction(eq_dec_points B O). right; assumption. left. apply (prod_uniquenessA O E E' A E B B H0); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum