proposition: Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b).
proof: Proof. intros a b Ha Hb. split; intros H. - destruct (sqrt_spec a Ha) as (LE,_). apply square_lt_simpl_nonneg; try order. - rewrite <- (sqrt_square b Hb) in H. now apply sqrt_lt_cancel. Qed.
imports: NZAxioms NZMulOrder