proposition: Lemma diff_uniquenessA : forall O E E' A A' B C, Diff O E E' A B C -> Diff O E E' A' B C -> A = A'.
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(opp_uniqueness O E E' H1 B); auto. subst mB'. apply (sum_uniquenessA O E E' H1 mB A A' C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg