proposition: Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)².
proof: Proof. intros a H. split. - now apply sqrt_spec. - le_elim H. + now apply sqrt_up_spec. + now rewrite <-H, sqrt_up_0, mul_0_l. Qed.
imports: NZAxioms NZMulOrder