proposition: Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a).
proof: Proof. intros a b Ha Hb. split; intros H. - destruct (sqrt_up_spec a) as (LE,LT). + apply le_lt_trans with b²; trivial using square_nonneg. + apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_square. Qed.
imports: NZAxioms NZMulOrder