proposition: Lemma a'_gt1 i : 1 < a' i.
proof: Proof. by rewrite exprn_egte1 // rootC_gt1 ?ltr1q ?ltr1n. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis