proposition: Lemma l14_36_b : forall O E E' A B C, Sum O E E' A B C -> Out O A B -> O <> A /\ O <> C /\ A <> C.
proof: Proof. intros. assert(HH:= l14_36_a O E E' A B C H H0). unfold Out in H0. spliter. split; auto. split. intro. subst C. apply between_identity in HH. subst A. tauto. intro. subst C. assert(HS:= H). unfold Sum in H. spliter. unfold Ar2 in H. spliter. assert(Sum O E E' A O A). apply (sum_A_O). assumption. assumption. assert(B = O). apply (sum_uniquenessB O E E' H A B O A); auto. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod