fact: Fixpoint Catalan_bin_leq n := if n is n.+1 then let cr := Catalan_bin_leq n in let new := sumn [seq nth 0 cr i * nth 0 cr (n - i) | i <- iota 0 n.+1] in rcons cr new else [:: 1].
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype