proposition: Lemma rho_h_iter (n : nat) : (2 <= n)%N -> rho n = h_iter n.
proof: Proof. elim: n => //; case => //; case => // [_ | n ihn] _. by rewrite rho2_eq; apply/eqP; rewrite /h_iter /= [_ == _]refines_eq. by rewrite -[in LHS]addn1 PoszD rho_rec // ihn. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) mathcomp(realalg) CoqEAL(hrel param refinements) CoqEAL(pos binnat binint rational) tactics shift binomialz bigopz rat_of_Z rho_computations seq_defs c_props initial_conds algo_closures