proposition: Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a).
proof: Proof. intros a b Ha Hb. split; intros H. - rewrite <- (sqrt_square b); trivial. now apply sqrt_le_mono. - destruct (sqrt_spec a Ha) as (LE,LT). transitivity (√a)²; trivial. now apply mul_le_mono_nonneg. Qed.
imports: NZAxioms NZMulOrder