proposition: Lemma opp_pos_neg : forall O E E' A MA, Ps O E A -> Opp O E E' A MA -> Ng O E MA.
proof: Proof. intros. assert(HH:=opp_midpoint O E E' A MA H0). unfold Ng. unfold Ps in H. unfold Out in H. unfold Midpoint in HH. spliter. repeat split; auto. intro. subst MA. apply cong_identity in H2. contradiction. induction H4. apply(outer_transitivity_between MA O A E); Between. apply(between_inner_transitivity MA O E A); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod