proposition: Lemma MOD_def : Nat.modulo = (@ε (arr (prod nat (prod nat nat)) (arr nat (arr nat nat'))) (fun r : (prod nat (prod nat nat)) -> nat -> nat -> nat => forall _3087 : prod nat (prod nat nat), forall m : nat, forall n : nat, @COND Prop (n = ( 0)) (((Nat.div m n) = ( 0)) /\ ((r _3087 m n) = m)) ((m = (Nat.add (Nat.mul (Nat.div m n) n) (r _3087 m n))) /\ (lt (r _3087 m n) n))) (@pair nat (prod nat nat) ( (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat ( (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) ( (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0))))))))))).
proof: Proof. generalize (@pair nat (prod nat nat) ( (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat ( (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) ( (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (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.modulo). intros x m n. destruct n. rewrite refl_is_True, COND_True. split; reflexivity. rewrite S_eq_0_is_False, COND_False. split. rewrite PeanoNat.Nat.mul_comm. apply Coq.Arith.PeanoNat.Nat.div_mod_eq. apply PeanoNat.Nat.mod_bound_pos. lia. lia. generalize (ε_spec i a). intro 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]. symmetry. exact h2. intro x. generalize (h x (S y)). rewrite S_eq_0_is_False, COND_False. intros [h1 h2]. generalize (Coq.Arith.PeanoNat.Nat.divmod_spec x y 0 y (le_n y)). unfold Nat.modulo. destruct (Nat.divmod x y 0 y) as [q r]. 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. rewrite (PeanoNat.Nat.mul_comm (S y) q) in i1. generalize (divmod_unicity (Nat.div x (S y)) q (S y) (ε Q a x (S y)) (y - r) h2 h3 i1). intros [j1 j2]. symmetry. exact j2. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat