proposition: Lemma halfa_uniqueness : forall O A B P P', HalfA P A O B -> HalfA P' A O B -> Out O P P'.
proof: Proof. intros O A B P P' HP HP'. apply halfa_chara1 in HP. apply halfa_chara1 in HP'. destruct HP as [A1 [M1]]. destruct HP' as [A2 [M2]]. spliter. assert (A1 = A2). { assert_diffs. apply (l6_11_uniqueness O O A B); auto. } subst A2. assert(M1 = M2) by (apply (l7_17 A A1); assumption). subst M2. apply l6_7 with M1; [apply l6_6|]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma