proposition: Lemma sum_to_sum3 : forall O E E' A B AB X S, Sum O E E' A B AB -> Sum O E E' AB X S -> sum3 O E E' A B X S.
proof: Proof. intros. unfold sum3. exists AB. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg