proposition: Lemma aux_positif : forall (k : R) (M : PO), O <> M :>PO -> k > 0 -> / Rsqr (distance O M) * k > 0.
proof: Proof. intros. apply Rmult_gt_0_compat; auto. apply Rgt_inv; auto. unfold Rsqr in |- *. assert (distance O M > 0). assert (distance O M >= 0); auto with geo. elim H1; intros; auto. absurd (distance O M = 0); auto with geo. apply Rmult_gt_0_compat; auto. Qed.