proposition: Lemma a_rec (n : nat) : a n = \prod_(0 <= i < n) a i + 1.
proof: Proof. elim: n => [|n Hn] //=; first by rewrite big_nil. by rewrite aS {2}Hn addn1 /= big_nat_recr //= mulnC addn1. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial