proposition: Lemma sqrt_lt_0_alt : forall x y : R, sqrt x < sqrt y -> x < y.
proof: Proof. intros x y. unfold sqrt at 2. destruct (Rcase_abs y) as [Hy|Hy]. - intros Hx. elim Rlt_not_le with (1 := Hx). apply sqrt_pos. - set (Hy' := Rge_le y 0 Hy). clearbody Hy'. clear Hy. unfold sqrt. destruct (Rcase_abs x) as [Hx|Hx]. + intros _. now apply Rlt_le_trans with R0. + intros Hxy. apply Rsqr_incrst_1 in Hxy ; try apply Rsqrt_positivity. unfold Rsqr in Hxy. now rewrite 2!Rsqrt_Rsqrt in Hxy. Qed.
imports: Rbase Rfunctions Rsqrt_def