proposition: Lemma big_nat_recr : forall n F, \big[*%M/1]_(0 <= i < n.+1) F i === (\big[*%M/1]_(0 <= i < n) F i) * F n.
proof: Proof. move=> n F; rewrite -> (@big_cat_nat n), ?leqnSn, big_nat1=> //; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops