proposition: Lemma eq_iteri f f' : f =2 f' -> forall n, iteri n f =1 iteri n f'.
proof: Proof. by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring