proposition: Fact le_0_a (k : int) : 0 <= a k.
proof: Proof. rewrite /a big_int_cond sumr_ge0 => // i ?; 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