proposition: Lemma div_uniqueness : forall A B C1 C2, div O E E' A B C1 -> div O E E' A B C2 -> C1 = C2.
proof: Proof. intros A B C1 C2 HC1 HC2. destruct HC1 as [IB [HIB HB1]]; destruct HC2 as [IB' [HIB' HC2]]. apply (inv_uniqueness B IB IB' HIB) in HIB'; treat_equalities. apply prod_uniqueness with O E E' A IB; assumption. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems