fact: Definition ba_casoratian (k : int) : rat := (b (int.shift 1 k) * a k) - b k * a (int.shift 1 k).
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics shift rat_of_Z seq_defs initial_conds algo_closures reduce_order a_props