proposition: Lemma a_rat_rec1 (n : nat) : (a (n.+1))%:Q = (a n)%:Q * ((a n)%:Q - 1) + 1.
proof: Proof. by rewrite aS -addn1 PoszD rmorphD /= PoszM rmorphM /= predn_int // rmorphB. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial