proposition: Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
proof: Proof. intros x y H H0; try assumption. case H; intros. - red; left. apply Rlt_mult_inv_pos; auto with real. - rewrite <- H1. red; right; ring. Qed.
imports: Rbase Rfunctions Rsqrt_def