proposition: Lemma sum3_uniqueness : forall O E E' A B C S1 S2, sum3 O E E' A B C S1 -> sum3 O E E' A B C S2 -> S1 = S2.
proof: Proof. intros. unfold sum3 in H. unfold sum3 in H0. ex_and H AB1. ex_and H0 AB2. assert(AB1 = AB2). apply(sum_uniqueness O E E' A B); auto. subst AB2. apply (sum_uniqueness O E E' AB1 C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg