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