proposition: Lemma ex_sums : forall A B C D, exists E F, SumS A B C D E F.
proof: Proof. intros A B C D. destruct (segment_construction A B C D) as [R [HR1 HR2]]. exists A, R, A, B, R. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines