proposition: Lemma big_nat_recl : forall n F, \big[op/idx]_(0 <= i < n.+1) F i === op (F 0) (\big[op/idx]_(0 <= i < n) F i.+1).
proof: Proof. by move=> n F; rewrite -> big_ltn=> //; rewrite -> big_add1;try reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops