proposition: Lemma affine_poly_pos_with_one (n : int) (b : rat) : 0 <= n -> b > 0 -> 0 < n%:Q + b.
proof: Proof. move=> ? ?. have <- : rat_of_Z 1 * n%:Q = n%:Q by rewrite rat_of_ZEdef mul1r. apply: affine_poly_pos => //. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics rat_of_Z