proposition: Fact a_incr (n m : int) : n <= m -> a n <= a m.
proof: Proof. move=> lenm. have [le0n | ltn0] := lerP 0 n; last by rewrite {1}/a big_geqz ?le_0_a; lia. have leSnSm : n + 1 <= m + 1 by lia. rewrite /a (big_cat_int _ _ _ _ leSnSm) //=; apply: ler_wpDr=> //; last first. rewrite [X in X <= _]big_int_cond [X in _ <= X]big_int_cond /=. apply: ler_sum => i; rewrite andbT => /andP [hi hin]; apply: c_incr; lia. rewrite big_int_cond; apply: sumr_ge0 => i; rewrite andbT => /andP [hni hmi]. by apply/ltW/lt_0_c; lia. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) mathcomp(realalg) CoqEAL(hrel param refinements) CoqEAL(pos binnat binint rational) tactics shift binomialz bigopz rat_of_Z rho_computations seq_defs c_props initial_conds algo_closures