proposition: Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b.
proof: Proof. intros a b Hab. destruct (lt_ge_cases a 0) as [Ha|Ha]. - rewrite (sqrt_neg _ Ha). apply sqrt_nonneg. - assert (Hb : 0 <= b) by order. destruct (sqrt_spec a Ha) as (LE,_). destruct (sqrt_spec b Hb) as (_,LT). apply lt_succ_r. apply square_lt_simpl_nonneg; try order. now apply lt_le_incl, lt_succ_r, sqrt_nonneg. Qed.
imports: NZAxioms NZMulOrder