proposition: Lemma sum3_exists : forall O E E' A B C, Ar2 O E E' A B C -> exists S, sum3 O E E' A B C S.
proof: Proof. intros. unfold Ar2 in *. spliter. assert(HH:=sum_exists O E E' H A B H0 H1). ex_and HH AB. assert(Ar2 O E E' A B AB). apply sum_ar2; auto. unfold Ar2 in H4. spliter. clean_duplicated_hyps. assert(HH:=sum_exists O E E' H AB C H7 H2). ex_and HH ABC. exists ABC. unfold sum3. exists AB. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg