proposition: Lemma diff_null_eq : forall O E E' A B, Diff O E E' A B O -> A = B.
proof: Proof. intros. assert(Ar2 O E E' A B O). apply diff_ar2; auto. unfold Ar2 in H0. spliter. clear H3. assert(Diff O E E' A A O). apply diff_null; Col. apply (diff_uniquenessB O E E' A _ _ O); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg