proposition: Lemma ltP_neg : forall O E E' A, LtP O E E' A O -> Ng O E A.
proof: Proof. intros O E E' A HLt. destruct HLt as [MA [HDiff HPs]]. apply opp_pos_neg with E' MA; auto. apply diff_O_A_opp; apply sum_diff; apply sum_comm; try apply diff_sum; auto. unfold Diff, Opp, Sum, Ar2 in HDiff; destruct HDiff as [MB HXMY]; spliter; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod