proposition: Lemma diff_uniqueness : forall O E E' A B D1 D2, Diff O E E' A B D1 -> Diff O E E' A B D2 -> D1 = D2.
proof: Proof. intros. assert(Ar2 O E E' A B D1). apply (diff_ar2); assumption. unfold Ar2 in H1. spliter. unfold Diff in *. ex_and H MB1. ex_and H0 MB2. assert(MB1 = MB2). apply (opp_uniqueness O E E' H1 B); assumption. subst MB2. apply(sum_uniqueness O E E' A MB1); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg