proposition: Lemma sum_A_exists : forall O E E' A AB, Ar2 O E E' A AB O -> exists B, Sum O E E' A B AB.
proof: Proof. intros. unfold Ar2 in *. spliter. assert(HH:=diff_exists O E E' AB A H H1 H0). ex_and HH B. exists B. apply diff_sum in H3. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg