proposition: Lemma lt_0_Ka : 0 < Ka.
proof: Proof. rewrite /Ka; apply: mulr_gt0; first exact: lt_0_a. apply: divr_gt0; last by rewrite exprn_gt0. rewrite big_int_cond; apply: prodr_gt0 => i; rewrite andbT => /andP [hi _]. exact/lt_0_rho/le_trans/hi. 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