proposition: Lemma iter_addr0 : forall n x, iter n (+%R (0 : R)) x = x.
proof: Proof. elim=> //= n IH x. by rewrite IH add0r. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2