proposition: Lemma sqrt_unique' : forall a b c, 0<=c<=2*b -> a == b² + c -> √a == b.
proof: Proof. intros a b c (Hc,H) EQ. apply sqrt_unique. rewrite EQ. split. - rewrite <- add_0_r at 1. now apply add_le_mono_l. - nzsimpl. apply lt_succ_r. rewrite <- add_assoc. apply add_le_mono_l. generalize H; now nzsimpl'. Qed.
imports: NZAxioms NZMulOrder