proposition: Lemma DIV_def : Nat.div = (@ε (arr (prod nat (prod nat nat)) (arr nat (arr nat nat'))) (fun q : (prod nat (prod nat nat)) -> nat -> nat -> nat => forall _3086 : prod nat (prod nat nat), exists r : nat -> nat -> nat, forall m : nat, forall n : nat, @COND Prop (n = ( 0)) (((q _3086 m n) = ( 0)) /\ ((r m n) = m)) ((m = (Nat.add (Nat.mul (q _3086 m n) n) (r m n))) /\ (lt (r m n) n))) (@pair nat (prod nat nat) ( (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat ( (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) ( (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))).
proof: Proof. generalize (@pair nat (prod nat nat) ( (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat ( (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) ( (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))); generalize (prod nat (prod nat (prod nat nat))); intros A a. match goal with [|- _ = ε ?x _] => set (Q := x) end. assert (i : exists q, Q q). exists (fun _ => Nat.div). intro x. exists Nat.modulo. intros m n. destruct (prop_degen (n=0)) as [h|h]; rewrite h. rewrite COND_True. rewrite is_True in h. rewrite h. simpl. split; reflexivity. rewrite COND_False. rewrite (PeanoNat.Nat.div_mod_eq m n) at 1. split. lia. rewrite is_False in h. apply PeanoNat.Nat.mod_bound_pos. lia. lia. generalize (ε_spec i a). intros [mod' h]. apply fun_ext; intro x. apply fun_ext; intro y. revert x. induction y. intro x. generalize (h x 0). rewrite refl_is_True, COND_True. intros [h1 h2]. rewrite h1. reflexivity. intro x. generalize (h x (S y)). rewrite S_eq_0_is_False, COND_False. intros [h1 h2]. simpl. generalize (Coq.Arith.PeanoNat.Nat.divmod_spec x y 0 y (le_n y)). destruct (Nat.divmod x y 0 y) as [q r]. simpl. rewrite PeanoNat.Nat.sub_diag, PeanoNat.Nat.mul_0_r, !PeanoNat.Nat.add_0_r. rewrite h1 at 1. intros [i1 i2]. assert (h3 : y - r < S y). lia. assert (e : q * S y = q + y * q). lia. rewrite <- e in i1. generalize (divmod_unicity (ε Q a x (S y)) q (S y) (mod' x (S y)) (y - r) h2 h3 i1). intros [j1 j2]. symmetry. exact j1. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat