proposition: Lemma sqrt_Rinv : forall x : R, x >= 0 -> x <> 0 -> sqrt (/ x) = / sqrt x.
proof: Proof. intros. inversion H. replace (/ x) with (1 / x); auto with real. rewrite sqrt_div; auto with real. rewrite sqrt_1. replace (1 / sqrt x) with (1 * / sqrt x); auto with real. replace (1 / x) with (1 * / x); auto with real. absurd (x = 0); auto. Qed.