proposition: Fact df_mexists_size n f : df_size (df_mexists n f) = n + df_size f.
proof: Proof. induction n as [ | n IHn ] in f |- *; auto; simpl. rewrite IHn; simpl; lia. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)