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