proposition: Fact df_mconj_size n f : df_size (df_mconj n f) = 4+n+∑ n (fun i => df_size (f i)).
proof: Proof. revert f; induction n as [ | n IHn ]; intros f; simpl; auto. rewrite IHn; ring. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)