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