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