proposition: Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
proof: Proof. intros x y H H0; try assumption. replace 0 with (x * 0). - apply Rmult_lt_compat_l; auto with real. - ring. Qed.
imports: Rbase Rfunctions Rsqrt_def