proposition: Lemma aux_negatif : forall (k : R) (M : PO), O <> M :>PO -> k < 0 -> / Rsqr (distance O M) * k < 0.
proof: Proof. intros. RReplace (/ Rsqr (distance O M) * k) (- (/ Rsqr (distance O M) * - k)). apply Ropp_lt_gt_0_contravar. apply aux_positif; auto with real. Qed.