proposition: Lemma pos_opp_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(Ar2 O E E' mA A O). unfold Opp in H0. apply sum_ar2; auto. unfold Ar2 in H1. apply opp_midpoint in H0. unfold Midpoint in H0. unfold Ps in H. unfold Out in H. spliter. unfold Ng. repeat split. intro. subst mA. apply H. apply cong_identity in H5. assumption. auto. induction H7. apply(outer_transitivity_between mA O A E); Between. apply between_symmetry. apply(between_exchange3 A E O mA); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod