proposition: Fact df_ren_size_Z ρ f : df_size_Z f⦃ρ⦄ = df_size_Z f.
proof: Proof. do 2 rewrite df_size_Z_spec; f_equal; apply df_ren_size. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)