proposition: Lemma prod_O_r_eq : forall O E E' A C, Prod O E E' A O C -> C = O.
proof: Proof. intros. assert(HH:=H). unfold Prod in HH. spliter. unfold Ar2 in H0. spliter. assert(HH:=prod_0_r O E E' A H0 H2). apply (prod_uniqueness O E E' A O); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum