proposition: Fact df_size_Z_spec f : df_size_Z f = Z.of_nat (df_size f).
proof: Proof. induction f as [ | | | ? f Hf g Hg | f Hf ]; simpl df_size; rewrite Nat2Z.inj_succ; try rewrite Nat2Z.inj_add; unfold df_size_Z; fold df_size_Z; auto; try lia. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)