Merge pull request #146 from trishullab/george

Modified 2018-2023 Coq formalizations.

coq/src/putnam_2018_a5.v

@@ -1,8 +1,10 @@
 Require Import Reals Coquelicot.Derive.
 Open Scope R_scope.
 Theorem putnam_2018_a5
-    (n : nat)
     (f: R -> R)
-    (x: R)
-    : (ex_derive_n f n x) -> f 0 = 0 /\ f 1 = 1 /\ (forall x, f x > 0) -> exists (n: nat) (x: R), gt n 0 -> ((Derive_n f n) x > 0).
+    (h0 : f 0 = 0)
+    (h1 : f 1 = 1)
+    (hpos : forall x : R, f x >= 0)
+    (hf : forall x : R, forall n : nat, ex_derive_n f n x)
+    : exists (n : nat) (x : R), gt n 0 /\ Derive_n f n x < 0.
 Proof. Admitted.

coq/src/putnam_2018_b2.v

@@ -1,12 +1,9 @@
-Require Import Reals. From Coqtail Require Import Cpow.
+Require Import Reals Coquelicot.Coquelicot Coquelicot.Hierarchy. From Coqtail Require Import Cpow.
 Open Scope C_scope.
 Theorem putnam_2018_b2
     (n : nat)
-    : forall (z : C), Cnorm z <= 1 -> ~exists z,
-    (fix f (n : nat) (z : C) (m : nat) : C :=
-        match m with
-        | O => 0
-        | S m' =>
-                (R_R_to_C (INR (n - m')) 0) * (z ^ m) + f n z m'
-    end) n z 0%nat = 0.
+    (hn : gt n 0)
+    (f : nat -> C -> C)
+    (hf : forall z : C, f n z = sum_n_m (fun i => (((RtoC (INR n)) - (RtoC (INR n))) * z ^ i)) 0 (n-1))
+    : forall (z : C), Cnorm z <= 1 -> f n z <> 0.
 Proof. Admitted.

coq/src/putnam_2018_b3.v

@@ -1,6 +1,6 @@
 Require Import Nat Ensembles. From mathcomp Require Import div seq ssrnat ssrbool.
-Definition solution_01 := fun n => n = 2^2 \/ n = 2^4 \/ n = 2^8 \/ n = 2^(16).
+Definition putnam_2018_b3_solution := fun n => n = 2^2 \/ n = 2^4 \/ n = 2^8 \/ n = 2^(16).
 Theorem putnam_2018_b3
-    (E : Ensemble nat := fun n => n > 0 -> (n < 10^(100)) /\ (n %| 2^n) /\ ((n-1) %| (2^n-1)) /\ ((n-2) %| (2^n-2)))
-    : E = solution_01.
+    (E : Ensemble nat := fun n => n > 0 /\ (n < 10^(100)) /\ (n %| 2^n) /\ ((n-1) %| (2^n-1)) /\ ((n-2) %| (2^n-2)))
+    : E = putnam_2018_b3_solution.
 Proof. Admitted.

coq/src/putnam_2018_b4.v

@@ -1,14 +1,13 @@
 Require Import Reals.
 Theorem putnam_2018_b4
     (a: R)
-    (n: nat)
-    (s := fix s (n:nat) (a: R) {struct n}: R :=
+    (s := fix s (n:nat) {struct n}: R :=
         match n with
         | O => R1
         | S O => a
         | S (S O) => a
         | S (S ((S n''') as n'') as n') =>
-                (2 * (s n' a) * (s n'' a) - (s n''' a))%R
+                (2 * (s n') * (s n'') - (s n'''))%R
     end)
-    : s n a = R0 -> forall (a: R), exists (m: nat) (n: nat), forall (i: nat), i >= m -> s (i+n) a = s i a.
+    : (exists n : nat, s n = R0) -> exists (T: nat), (gt T 0 /\ forall (i: nat), s (i+T) = s i).
 Proof. Admitted.

coq/src/putnam_2019_b2.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2019_b2_solution := 8 / PI ^ 3.
 Theorem putnam_2019_b2 
-    (a : nat -> R := fun n => sum_n (fun k => let k := INR k in let n := INR n in (sin (2 * (k + 1) * PI / (2 * n))) / ((cos ((k - 1) * PI / (2 * n))) ^ 2 * (cos ((k * PI) / (2 * n))) ^ 2)) (n - 1))
+    (a : nat -> R := fun n => sum_n_m (fun k => let k := INR k in let n := INR n in (sin (2 * (k + 1) * PI / (2 * n))) / ((cos ((k - 1) * PI / (2 * n))) ^ 2 * (cos ((k * PI) / (2 * n))) ^ 2)) 1 (n - 1))
     : Lim_seq (fun n => a n / INR n ^ 3) = putnam_2019_b2_solution.
 Proof. Admitted.

coq/src/putnam_2020_a2.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2020_a2_solution := fun k => 4 ^ k.
 Theorem putnam_2020_a2  
-    : (fun k => sum_n (fun j => 2 ^ (k - j) * Binomial.C (k + j) j) (k + 1)) = putnam_2020_a2_solution.
+    : (fun k => sum_n (fun j => 2 ^ (k - j) * Binomial.C (k + j) j) k) = putnam_2020_a2_solution.
 Proof. Admitted.

coq/src/putnam_2020_b1.v

@@ -8,6 +8,6 @@ Theorem putnam_2020_b1
         | xO n' => d n'%positive
         | xI n' => 1 + d n'%positive
     end)
-    (A := sum_n (fun k => IZR ((-1) ^ (d (Pos.of_nat (S k))) * (Z.of_nat k) ^ 3)) 2020)
+    (A := sum_n_m (fun k => IZR ((-1) ^ (d (Pos.of_nat (S k))) * (Z.of_nat k) ^ 3)) 1 2020)
     : (floor A) mod 2020 = putnam_2020_b1_solution.
 Proof. Admitted.

coq/src/putnam_2020_b5.v

@@ -1,12 +1,8 @@
 From mathcomp Require Import fintype seq ssrbool. Require Import Reals Coquelicot.Complex.
 Open Scope C.
 Theorem putnam_2020_b5
-    (z: 'I_4 -> C)
-    (i0 n: 'I_4)
-    : (Cmod (z n) < 1)%R /\
-    z n <> RtoC 1 ->
-    RtoC 3 - z (nth i0 (enum 'I_4) 0) - z (nth i0 (enum 'I_4) 1) -
-    z (nth i0 (enum 'I_4) 2) - z (nth i0 (enum 'I_4) 3) +
-    z (nth i0 (enum 'I_4) 0) * z (nth i0 (enum 'I_4) 1) *
-    z (nth i0 (enum 'I_4) 2) * z (nth i0 (enum 'I_4) 3) <> RtoC 0.
+    (z1 z2 z3 z4 : C)
+    (hznorm : Cmod z1 = 1%R /\ Cmod z2 = 1%R /\ Cmod z3 = 1%R /\ Cmod z4 = 1%R)
+    (hzne : z1 <> RtoC 1 /\ z2 <> RtoC 1 /\ z3 <> RtoC 1 /\ z4 <> RtoC 1)
+    : RtoC 3 - z1 - z2 - z3 - z4 + z1 * z2 * z3 * z4 <> RtoC 0.
 Proof. Admitted.

coq/src/putnam_2020_b6.v

@@ -2,7 +2,6 @@ Require Import Reals. From Coquelicot Require Import Coquelicot Hierarchy Rcompl
 Open Scope R.
 Theorem putnam_2020_b6 
     (A : nat -> R := fun k => (-1)^(Z.to_nat (floor (INR k * (sqrt 2 - 1)))))
-    (B : nat -> R := fun n => sum_n A n)
+    (B : nat -> R := fun n => sum_n_m A 1 n)
     : forall (n: nat), B n >= 0.
-Proof. Admitted. 
-End putnam_2020_b6.
+Proof. Admitted. 

coq/src/putnam_2021_a2.v

@@ -3,7 +3,7 @@ Open Scope R.
 Definition putnam_2021_a2_solution := exp 1.
 Theorem putnam_2021_a2
     (sequence_r_to_0 : nat -> R := fun n => 1 / INR n)
-    (f : R -> R -> R := fun r x => Rpower (Rpower(x+1)(r+1) - Rpower x (r+1)) 1/r)
+    (f : R -> R -> R := fun r x => Rpower (Rpower (x+1) (r+1) - Rpower x (r+1)) 1/r)
     (g : R -> R := fun x => Lim_seq (fun n => f (sequence_r_to_0 n) x))
     : Lim_seq (fun n => (g (INR n))/INR n) = putnam_2021_a2_solution.
 Proof. Admitted. 

coq/src/putnam_2021_a4.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2021_a4_solution := (sqrt 2 / 2) * PI * ln 2 / ln 10.
 Theorem putnam_2021_a4 
-    (I : nat -> R := fun r => RInt (fun x => RInt (fun y => (1 + 2 * x ^ 2) / (1 + x ^ 4 + 6 * x ^ 2 * y ^ 2 + y ^ 4) - (1 + y ^ 2) / (2  + x ^ 4 + y ^ 4)) 0 (sqrt (INR r ^ 2 - x ^ 2))) 0 1)
-    : ~ ex_lim_seq I \/ Lim_seq I = putnam_2021_a4_solution.
+    (I : nat -> R := fun r => RInt (fun x => RInt (fun y => (1 + 2 * x ^ 2) / (1 + x ^ 4 + 6 * x ^ 2 * y ^ 2 + y ^ 4) - (1 + y ^ 2) / (2  + x ^ 4 + y ^ 4)) 0 (sqrt (INR r ^ 2 - x ^ 2))) 0 r)
+    : Lim_seq I = putnam_2021_a4_solution.
 Proof. Admitted.

coq/src/putnam_2022_a6.v

@@ -7,7 +7,7 @@ Theorem putnam_2022_a6
     (i0 : 'I_n)
     (sumIntervals : ('I_n -> R) -> nat -> R := fun s k => sum_n (fun i => (((s (nth i0 (enum 'I_n) (i+1))))^(2*k-1) - ((s (nth i0 (enum 'I_n) i)))^(2*k-1))) (n-1))
     (valid : nat -> ('I_n -> R) -> Prop := fun m s => forall (k: nat), and (le 1 k) (le k m) -> sumIntervals s k = 1)
-    (hvalid : nat -> Prop := fun m => exists (s : 'I_n -> R), (forall (i : 'I_n),  s i < s (ordS i)) /\ s (nth i0 (enum 'I_n) 0) > -1 /\ s (nth i0 (enum 'I_n) (n-1)) < 1 -> valid m s)
+    (hvalid : nat -> Prop := fun m => exists (s : 'I_n -> R), (forall (i : 'I_n),  (s i < s (ordS i)) /\ s (nth i0 (enum 'I_n) 0) > -1 /\ s (nth i0 (enum 'I_n) (n-1)) < 1) -> valid m s)
     (hM : hvalid M)
     (hMub : forall m : nat, hvalid m -> le m M)
     : M = putnam_2022_a6_solution n.

coq/src/putnam_2022_b2.v

@@ -1,14 +1,14 @@
-Require Import Ensembles Finite_sets List Reals.
+Require Import Ensembles Finite_sets Reals.
 Require Import GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions.
 Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
-Import ListNotations.
+(* Import ListNotations. *)
 Definition vect3:= (F * F * F)%type.
 Definition cross_prod (v w : vect3) :=  let '(v1, v2, v3) := v in let '(w1, w2, w3) := w in 
    (SubF (MulF v2 w3) (MulF v3 w2),
     SubF (MulF v3 w1) (MulF v1 w3),
     SubF (MulF v1 w2) (MulF v2 w1)).
-Definition putnam_2022_b2_solution := [1; 7].
+Definition putnam_2022_b2_solution : Ensemble nat := fun n => n = 1 \/ n = 7.
 Theorem putnam_2022_b2
-    (p : nat -> Prop := fun n => exists (A: Ensemble vect3), forall (u: vect3), A u <-> exists (v w: vect3), u = cross_prod v w /\ cardinal vect3 A n)
-    : forall (n: nat), n > 0 /\ p n -> In n putnam_2022_b2_solution.
+    (p : nat -> Prop := fun n => exists (A: Ensemble vect3), cardinal vect3 A n /\ (forall (u: vect3), A u <-> exists (v w: vect3), u = cross_prod v w))
+    : forall (n: nat), (n > 0 /\ p n) <-> In _ putnam_2022_b2_solution n.
 Proof. Admitted. 

coq/src/putnam_2022_b6.v

@@ -3,7 +3,7 @@ Open Scope R.
 Definition putnam_2022_b6_solution := fun (f : R -> R) =>
     exists (c : R), c >= 0 /\ forall (x : R), x >= 0 /\ f x >= 0 -> f x = 1 / (1 + c * x).
 Theorem putnam_2022_b6
-    (p : (R -> R) -> Prop := fun f : R -> R => forall (x y: R), x > 0 /\ y > 0 /\ f x > 0 /\ f y > 0 ->
-        f (x * f y) + f (y * f x) = 1 + f (x + y))
+    (p : (R -> R) -> Prop := fun f : R -> R => forall (x y: R), (x > 0 /\ y > 0 /\ f x > 0 /\ f y > 0) ->
+        (continuity_pt f x /\ f (x * f y) + f (y * f x) = 1 + f (x + y)))
     : forall f : R -> R, p f <-> putnam_2022_b6_solution f.
 Proof. Admitted. 

coq/src/putnam_2023_a1.v

@@ -1,17 +1,12 @@
 Require Import Reals List Rtrigo_def Coquelicot.Derive.
 Open Scope R.
-Definition min_sol : nat := 18.
+Definition putnam_2023_a1_solution : nat := 18.
 Theorem putnam_2023_a1
-    (n: nat)
-    (hn : gt n 0)
-    : Rabs ((Derive_n (fun x =>
-        let f_i i := cos (INR i * x) in
-        let coeffs := map f_i (seq 1 n) in
-        fold_right Rmult 1 coeffs) 2) 0) > 2023 ->
-    (n >= min_sol)%nat /\
-    Rabs ((Derive_n (fun x =>
-        let f_i i := cos (INR i * x) in
-        let coeffs := map f_i (seq 1 min_sol) in
-        fold_right Rmult 1 coeffs) 2) 0) > 2023. 
-Proof. Admitted.
+    (f : nat -> R -> R := fun n (x : R) => 
+        let f_i i := cos (INR i * x) in 
+            let coeffs := map f_i (seq 1 n) in 
+                fold_right Rmult 1 coeffs
+    )
+    : gt putnam_2023_a1_solution 0 /\ Derive_n (f putnam_2023_a1_solution) 2 0 > 2023 /\ (forall n : nat, (gt n 0 /\ lt n putnam_2023_a1_solution) -> Derive_n (f n) 2 0 <= 2023).
+Proof. Admitted. 
 

coq/src/putnam_2023_a2.v

@@ -1,12 +1,12 @@
 Require Import Nat Ensembles Factorial Reals Coquelicot.Coquelicot.
-Definition putnam_2023_a2_solution : Ensemble R := fun x => exists (n: nat), x = -1 / INR (fact n) \/ x = 1 / INR (fact n).
+Definition putnam_2023_a2_solution : nat -> Ensemble R := (fun n => (fun x => x = -1 / INR (fact n) \/ x = 1 / INR (fact n))).
 Theorem putnam_2023_a2 
     (n : nat)
     (hn0 : gt n 0)
     (hnev : even n = true)
     (coeff: nat -> R)
-    (p : R -> R := fun x => sum_n (fun i => coeff i * x ^ i) (2 * n + 1))
+    (p : R -> R := fun x => sum_n (fun i => coeff i * x ^ i) (2 * n))
     (monic_even : coeff (mul 2 n) = 1)
     (hpinv : forall k : Z, and (Z.le 1 (Z.abs k)) (Z.le (Z.abs k) (Z.of_nat n)) -> p (1 / (IZR k)) = IZR (k ^ 2))
-    : (fun x => (p (1 / x) = x ^ 2 /\ ~ exists k : Z, x = IZR k /\ Z.le (Z.abs k) (Z.of_nat n))) = putnam_2023_a2_solution.
+    : (fun x => (p (1 / x) = x ^ 2 /\ ~ exists k : Z, x = IZR k /\ Z.le (Z.abs k) (Z.of_nat n))) = putnam_2023_a2_solution n.
 Proof. Admitted.

coq/src/putnam_2023_a3.v

@@ -1,9 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2023_a3_solution := PI / 2.
 Theorem putnam_2023_a3 
-    (r : R)
-    (hr : r > 0)
-    (p : R -> Prop := fun t => exists (f g : R -> R), f 0 = 0 /\ g 0 = 0 /\ forall (x: R), Rabs (Derive f x) <= Rabs (g x) /\ forall (x: R), Rabs (Derive g x) <= Rabs (f x) /\ f t = 0)
-    : (forall (t: R), t > 0 -> t < r -> ~ (p t)) <-> r = putnam_2023_a3_solution.
-Proof. Admitted.
-End putnam_2023_a3.
+    (p : R -> Prop := fun t => exists (f g : R -> R), f 0 > 0 /\ g 0 = 0 /\ (forall (x : R), ex_derive f x /\ ex_derive g x) /\ (forall (x: R), (Rabs (Derive f x) <= Rabs (g x) /\ Rabs (Derive g x) <= Rabs (f x))) /\ f t = 0)
+    : (putnam_2023_a3_solution > 0 /\ p putnam_2023_a3_solution) /\ (forall (t: R), t > 0 -> t < putnam_2023_a3_solution -> ~ (p t)).
+Proof. Admitted.

coq/src/putnam_2023_b2.v

@@ -1,12 +1,12 @@
 Require Import BinNums Nat NArith.
 Definition putnam_2023_b2_solution := 3.
 Theorem putnam_2023_b2
-    (k:= fix count_ones (n : positive) : nat :=
+    (k := fix count_ones (n : positive) : nat :=
         match n with
         | xH => 1
         | xO n' => count_ones n'
         | xI n' => 1 + count_ones n'
     end)
-    : (forall (n: nat), k (Pos.of_nat (2023*n)) >= putnam_2023_b2_solution) /\
-    (exists (n: nat), k (Pos.of_nat (2023*n)) = putnam_2023_b2_solution).
+    : (forall (n: nat), n > 0 -> k (Pos.of_nat (2023*n)) >= putnam_2023_b2_solution) /\
+    (exists (n: nat), n > 0 /\ k (Pos.of_nat (2023*n)) = putnam_2023_b2_solution).
 Proof. Admitted.

coq/src/putnam_2023_b4.v

@@ -2,17 +2,18 @@ Require Import Reals Coquelicot.Derive Coquelicot.Hierarchy. From mathcomp Requi
 Definition putnam_2023_b4_solution := 29.
 Theorem putnam_2023_b4 
     (n : nat)
+    (hn : gt n 0)
     (i0 : 'I_n)
     (s : 'I_n -> R)
     (f : R -> R)
     (t0 := s (nth i0 (enum 'I_n) 0))
     (hs : forall i : 'I_n, s i < s (ordS i))
     (hf : forall t : R, 
-        ((t >= t0 -> continuity_pt f t) /\ (t > t0 /\ ~ exists i, s i = t -> ex_derive_n f 2 t)) /\ 
+        ((t >= t0 -> continuity_pt f t) /\ ((t > t0 /\ ~ exists i, s i = t) -> ex_derive_n f 2 t)) /\ 
         (f t0 = 0.5) /\
         (forall k: 'I_n, let tk := s k in filterlim (Derive_n f 1) (at_right tk) (locally 0)) /\
-        (forall k: 'I_n, k <> nth i0 (enum 'I_n) (n-1) -> let tk := s k in tk < t < tk+1 -> (Derive_n f 2) = (fun _ => INR k+1)) /\ 
-        (forall m: 'I_n, t > s (nth i0 (enum 'I_n) m) -> (Derive_n f 2) = (fun _ => INR m+1))
+        (forall k: 'I_n, k <> nth i0 (enum 'I_n) (n-1) -> let tk := s k in tk < t < tk+1 -> (Derive_n f 2) t = INR k+1) /\ 
+        (forall m: 'I_n, t > s (nth i0 (enum 'I_n) m) -> (Derive_n f 2) t INR m+1)
     )
     : forall (T: R), f(t0+T) = 2023 <-> T >= putnam_2023_b4_solution /\ f(t0 + putnam_2023_b4_solution) = 2023.
 Proof. Admitted. 

coq/src/putnam_2023_b5.v

@@ -1,6 +1,6 @@
 Require Import PeanoNat. From mathcomp Require Import div fintype perm ssrbool.
 Definition putnam_2023_b5_solution (n : nat) := n = 1 \/ n mod 4 = 2.
 Theorem putnam_2023_b5
-    (p : nat -> Prop := fun n => forall m : nat, coprime m n -> exists (π: {perm 'I_n}), forall (k: 'I_n), (π (π k))%%n mod n = m*k%%n)
-    : forall n : nat, p n <-> putnam_2023_b5_solution n.
-Proof. Admitted. 
+    (p : nat -> Prop := fun n => forall m : nat, coprime m n -> exists (π: {perm 'I_n}), forall (k: 'I_n), nat_of_ord (π (π k)) = (m*(nat_of_ord k))%%n)
+    : forall n : nat, (n > 0 /\ p n) <-> putnam_2023_b5_solution n.
+Proof. Admitted. 

isabelle/putnam_2021_b2.thy

@@ -10,5 +10,4 @@ theorem putnam_2021_b2:
   shows "(GREATEST Sa::real. (\<exists>a::nat\<Rightarrow>real. asum a \<and> S a = Sa)) = putnam_2021_b2_solution"
   sorry
 
-
 end

isabelle/putnam_2023_a5.thy

@@ -7,7 +7,7 @@ definition putnam_2023_a5_solution :: "complex set" where "putnam_2023_a5_soluti
 theorem putnam_2023_a5:
   fixes num_ones :: "nat \<Rightarrow> nat"
   assumes h0 : "num_ones 0 = 0"
-    and hi : "\<forall> n > 0. num_ones n = (num_ones (n div 3)) + (if [n = 1] (mod 3) then 1 else 0)"
+    and hi : "\<forall> n > 0. num_ones n = (if [n = 1] (mod 3) then 1 else 0) + (num_ones (n div 3))"
   shows "{z :: complex. (\<Sum> k=0..(3^1010 - 1). ((-2)^(num_ones k) * (z + k)^2023)) = 0} = putnam_2023_a5_solution"
   sorry
 

isabelle/putnam_2023_b2.thy

@@ -7,7 +7,7 @@ definition putnam_2023_b2_solution :: "nat" where "putnam_2023_b2_solution \<equ
 theorem putnam_2023_b2:
   fixes ones :: "nat \<Rightarrow> nat"
   assumes h0 : "ones 0 = 0"
-    and hi : "\<forall> n > 0. ones n = ones (n div 2) + (if [n = 1] (mod 2) then 1 else 0)"
+    and hi : "\<forall> n > 0. ones n = (if [n = 1] (mod 2) then 1 else 0) + ones (n div 2)"
   shows "(LEAST k :: nat. \<exists> n > 0. ones (2023*n) = k) = putnam_2023_b2_solution"
   sorry
 

lean4/src/putnam_2020_b6.lean

@@ -6,5 +6,5 @@ open Filter Topology Set
 theorem putnam_2020_b6
 (n : ℕ)
 (npos : n > 0)
-: ∑ k : Fin n, ((-1) ^ Int.floor ((k.1 + 1) * (Real.sqrt 2 - 1)) : ℝ) ≥ 0 :=
+: ∑ k in Finset.Icc 1 n, ((-1) ^ Int.floor (k * (Real.sqrt 2 - 1)) : ℝ) ≥ 0 :=
 sorry

lean4/src/putnam_2021_b4.lean

@@ -7,5 +7,5 @@ theorem putnam_2021_b4
 (F : ℕ → ℕ)
 (hF : ∀ x, x ≥ 2 → F x = F (x - 1) + F (x - 2))
 (F01 : F 0 = 0 ∧ F 1 = 1)
-: ∀ m, m > 2 → (∃ p,  (∏ k : Set.Icc 1 (F m - 1),  (k.1 ^ k.1))  % F m = F p) :=
+: ∀ m, m > 2 → (∃ p,  (∏ k : Set.Icc 1 (F m - 1),  (k.1 ^ k.1)) % F m = F p) :=
 sorry