proposition: Lemma sum_iff_cong : forall A B C, Ar2 O E E' A B C -> (O <> C \/ B <> A) -> ((Cong O A B C /\ Cong O B A C) <-> Sum O E E' A B C).
proof: Proof. intros. split. intros. apply cong_sum;intuition idtac. intros. apply sum_cong2. assumption. destruct H. elim (eq_dec_points A O); intro. subst. right. intro. subst. assert (T:= sum_O_O). destruct H0. apply H0. eauto using sum_uniqueness. intuition. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg