proposition: Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b).
proof: Proof. intros a b Ha Hb. split; intros H. - rewrite <- (sqrt_up_square b Hb). now apply sqrt_up_le_mono. - apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg]. transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec. Qed.
imports: NZAxioms NZMulOrder