proposition: Lemma Rsqr_bounds_le : 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_le; assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun