proposition: Lemma Rsqr_bounds_lt : forall a b:R, -a < b < a -> 0 <= Rsqr b < Rsqr a.
proof: Proof. intros a b [H1 H2]. split. - apply Rle_0_sqr. - apply neg_pos_Rsqr_lt; assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun