proposition: Fact lt_0_ba_casoratian (n : nat) : 0 < 6%:Q / (n%:Q + 1%:Q) ^ 3.
proof: Proof. by apply/divr_gt0/exprn_gt0 => //; rewrite -rmorphD ltr0n addn1. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics shift rat_of_Z seq_defs initial_conds algo_closures reduce_order a_props