proposition: Lemma diff_uniquenessB : forall O E E' A B B' C, Diff O E E' A B C -> Diff O E E' A B' C -> B = B'.
proof: Proof. intros. assert(Ar2 O E E' A B C). apply diff_ar2; auto. assert(Ar2 O E E' A B' C). apply diff_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. unfold Diff in *. ex_and H mB. ex_and H0 mB'. assert(mB = mB'). apply (sum_uniquenessA O E E' H1 A mB mB' C); apply sum_comm; auto. subst mB'. apply (opp_uniqueness O E E' H1 mB); apply opp_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg