proposition: Lemma sum_pos_null : forall O E E' A B, ~Ng O E A -> ~Ng O E B -> Sum O E E' A B O -> A = O /\ B = O.
proof: Proof. intros. assert(Col O E A /\ Col O E B /\ O <> E /\ ~Col O E E'). { unfold Sum in H1. unfold Ar2 in H1. spliter. repeat split;Col. intro. subst E. Col. } spliter. assert(Ps O E A \/ A = O). { induction(eq_dec_points A O). { right; auto. } { left. apply (not_neg_pos O E A) in H; Col. induction H. { auto. } { contradiction. } } } assert(Ps O E B\/ B = O). { induction(eq_dec_points B O). { right; auto. } { left. apply (not_neg_pos O E B) in H0; Col. induction H0. { auto. } { contradiction. } } } induction H6; induction H7. { assert(HH:= sum_pos_pos O E E' A B O H6 H7 H1). unfold Ps in HH. unfold Out in HH. tauto. } { subst B. assert(HH:=sum_A_O O E E' H5 A H2). split; auto. apply (sum_uniqueness O E E' A O); auto. } { subst A. assert(HH:=sum_O_B O E E' H5 B H3). split; auto. apply (sum_uniqueness O E E' O B );auto. } { tauto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order