proposition: Lemma affine_poly_pos (n : int) (a b : rat) : 0 <= n -> a > 0 -> b > 0 -> 0 < a * n%:Q + b.
proof: Proof. move=> le_0_n pos_a pos_b. apply: (@lt_le_trans _ _ b) => //. rewrite ler_addr mulr_ge0 //. by rewrite le0r pos_a orbT. by rewrite ler0z. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics rat_of_Z