proposition: Lemma rho_maj (n : nat) : (N_rho < n)%N -> 33%:Q < rho n.
proof: Proof. move=> lt_Nrho_n; rewrite -compat33; apply: lt_le_trans lt_33_r51 _. by apply: rho_incr => //; rewrite lez_nat; apply: leq_trans lt_Nrho_n. 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