proposition: Lemma a'_ge0 i : 0 <= a' i.
proof: Proof. exact: ltW. 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