proposition: Lemma a_rat_rec (n : nat): a_rat n = \prod_ (0 <= i < n) (a_rat i) + 1.
proof: Proof. by rewrite /= /a_rat a_rec PoszD rmorphD /= prodMz. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial