proposition: Lemma pos_null_neg : forall O E E' A MA, Opp O E E' A MA -> Ps O E A \/ O = A \/ Ps O E MA.
proof: Proof. intros. unfold Opp in H. induction (eq_dec_points A O). right; left; auto. assert(HS:= H). unfold Sum in H. spliter. unfold Ar2 in H. spliter. assert(Parallelogram_flat O MA O A). apply(sum_cong O E E' H MA A O HS); tauto. unfold Parallelogram_flat in H5. spliter. assert(HG:=grid_not_par O E E' H). spliter. assert(A = MA \/ Midpoint O A MA). apply(l7_20 O A MA); Col. induction H16. subst MA. tauto. induction(out_dec O E A). left. unfold Ps. apply l6_6. assumption. right; right. assert(MA <> O). intro. subst MA. apply is_midpoint_id_2 in H16. subst A. tauto. unfold Midpoint in H16. spliter. unfold Ps. unfold Col in H2. induction H2. unfold Out. repeat split; auto. induction H2. unfold Out. repeat split; Col. left. apply between_symmetry. auto. apply False_ind. apply H17. unfold Out. repeat split; auto. apply between_symmetry in H16. assert(HH:= l5_2 MA O A E H18 H16 H2). tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod