proposition: Lemma sum_A_O_eq : forall A C, Sum O E E' A O C -> A = C.
proof: Proof. intros. assert (HS:=H). unfold Sum in H. spliter. unfold Ar2 in H. spliter. assert(HH:=sum_A_O A H1). apply (sum_uniqueness A O); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg