proposition: Lemma finite_diff_pos (a b : int -> rat) : is_fdiff_of b a -> a 0 > 0 -> (forall n : int, n >= 0 -> b n > 0) -> (forall n : int, n >= 0 -> a n > 0).
proof: Proof. move=> fdiff a0_pos cond_bn_pos n. case: n => [o | //]. elim: o; first done. move=> o. set n := (Posz o). have -> : Posz o.+1 = n + 1 by rewrite intS addrC. have : n >= 0 by done. move=> n_nonneg cond_an_pos _. move: {cond_an_pos} (cond_an_pos n_nonneg) => an_pos. move: {cond_bn_pos} (cond_bn_pos n n_nonneg) => bn_pos. move: {fdiff} (fdiff n n_nonneg) => fdiff. rewrite -{}fdiff in bn_pos. have -> : a (n + 1) = a (n + 1) - a n + a n by ring. apply: (ltr_spsaddl bn_pos an_pos). Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics rat_of_Z