proposition: Lemma Rgt_inv : forall k : R, k > 0 -> / k > 0.
proof: Proof. intros. cut (k <> 0); intros; [ idtac | auto with real ]. cut (k >= 0); intros. cut (/ k >= 0); intros. 2: apply Rinv_le_pos; auto. elim H2; intros; auto. absurd (/ k = 0); auto with real. red in |- *. left; try assumption. Qed.