proposition: Lemma inv_uniqueness : forall A B1 B2, inv O E E' A B1 -> inv O E E' A B2 -> B1 = B2.
proof: Proof. intros A B1 B2 HB1 HB2; elim (eq_dec_points A O); intro HNEq; [induction HB1; induction HB2; spliter; treat_equalities; intuition|]. subst;auto. elim HB1; clear HB1; intro HB1; [clear HNEq|spliter; subst; intuition]. elim HB2; clear HB2; intro HB2; [|spliter; subst; intuition]. destruct HB1 as [HNEq HB1]; destruct HB2 as [H HB2]; clear H. apply prod_uniquenessA with O E E' A E; 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