proposition: Fact df_mconj_spec n f ν : df_pred (df_mconj n f) ν <-> forall i, i < n -> df_pred (f i) ν.
proof: Proof. revert f ν; induction n as [ | n IHn ]; intros f v; simpl df_mconj. + rewrite df_true_spec; split; auto; intros; lia. + rewrite df_pred_conj, IHn; split. * intros (? & H2) [ | i ] ?; auto; apply H2; lia. * intros H; split; intros; apply H; lia. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)