proposition: Lemma df_mexists_spec n f ν : ⟦df_mexists n f⟧ ν <-> exists π, ⟦f⟧ (fun i => if le_lt_dec n i then ν (i-n) else π i).
proof: Proof. revert f ν; induction n as [ | n IHn ]; intros f v. + simpl; split; [ intros H; exists (fun _ => 0) | intros (? & H) ]; revert H; apply df_pred_ext; intros; f_equal; lia. + simpl df_mexists; rewrite IHn; split; intros (pi & Hpi). * revert Hpi; rewrite df_pred_exst. intros (u & Hu). exists (fun i => match i with 0 => u | S i => pi i end). revert Hu; apply df_pred_ext. Opaque le_lt_dec. simpl; intros [ | i ]. - replace (0-S n) with 0 by lia; auto. - replace (S i - S n) with (i-n) by lia. simpl; destruct (le_lt_dec (S n) (S i)); destruct (le_lt_dec n i); auto; lia. * exists (fun i => pi (S i)). rewrite df_pred_exst; exists (pi 0). revert Hpi; apply df_pred_ext. intros [ | i ]. - replace (0-S n) with 0 by lia; simpl; auto. - replace (S i - S n) with (i-n) by lia. Opaque le_lt_dec. simpl; destruct (le_lt_dec (S n) (S i)); destruct (le_lt_dec n i); auto; lia. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)