proposition: Lemma diff_pos_diff_neg : forall O E E' A B AmB BmA, Diff O E E' A B AmB -> Diff O E E' B A BmA -> Ps O E AmB -> Ng O E BmA.
proof: Proof. intros. assert(Opp O E E' AmB BmA). apply (diff_opp O E E' A B); auto. eapply (pos_opp_neg O E E' AmB); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod