From 7dff68d18f2c9d0d173df8189e43cdfc20155f65 Mon Sep 17 00:00:00 2001
From: qvermande <quentin.vermande@ens.psl.eu>
Date: Tue, 25 Jul 2023 13:13:23 +0200
Subject: [PATCH] remove duplicate in map_gal; remove temp

---
 _CoqProject                  |  1 -
 theories/xmathcomp/map_gal.v |  2 --
 theories/xmathcomp/temp.v    | 38 ------------------------------------
 theories/xmathcomp/various.v | 15 +++++---------
 4 files changed, 5 insertions(+), 51 deletions(-)
 delete mode 100644 theories/xmathcomp/temp.v

diff --git a/_CoqProject b/_CoqProject
index 57140ef..0289931 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,7 +7,6 @@ theories/xmathcomp/char0.v
 theories/xmathcomp/cyclotomic_ext.v
 theories/xmathcomp/real_closed_ext.v
 theories/xmathcomp/artin_scheier.v
-theories/xmathcomp/temp.v
 
 -R theories Abel
 -arg -w -arg -projection-no-head-constant
diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v
index d67ac6d..9febe38 100644
--- a/theories/xmathcomp/map_gal.v
+++ b/theories/xmathcomp/map_gal.v
@@ -19,8 +19,6 @@ Import AEnd_FinGroup.
 Variables (F0 : fieldType) (L : splittingFieldType F0).
 Implicit Types (K E F : {subfield L}).
 
-Lemma galois_subW E F : galois E F -> (E <= F)%VS. Proof. by case/andP. Qed.
-
 Lemma galois_normalW E F : galois E F -> (normalField E F)%VS.
 Proof. by case/and3P. Qed.
 
diff --git a/theories/xmathcomp/temp.v b/theories/xmathcomp/temp.v
deleted file mode 100644
index 341f5dd..0000000
--- a/theories/xmathcomp/temp.v
+++ /dev/null
@@ -1,38 +0,0 @@
-From mathcomp Require Import all_ssreflect.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Section Temp.
-
-(* This is actually quite useless, I am not convinced anymore that we should keep it. *)
-Lemma big_condT [R : Type] [idx : R] (op : Monoid.com_law idx)
-    [I : finType] (A : {pred I}) (F : I -> R) :
-    \big[op/idx]_(i in A | true) F i = \big[op/idx]_(i in A) F i.
-Proof. by rewrite big_mkcondr. Qed.
-
-(** Alternative: *)
-(* Definition Zp_succ n : 'I_n -> 'I_n := if n is n.+1 then +%R ord_max else id. *)
-(* The computational content would not be visible without the case distinction on n. Besides, this is not used anywhere anymore, so we can get rid of it. *)
-
-Definition Zp_succ n (i : 'I_n) :=
-  match i with
-  | @Ordinal _ k klt => Ordinal (
-      match n as n0 return (k < n0)%N -> (k.+1 %% n0 < n0)%N with
-      | 0 => id
-      | n0.+1 => fun=> ltn_pmod k.+1 (is_true_true : 0 < n0.+1)%N
-      end klt)
-  end.
-
-(* J'ai l'impression que je veux garder la quantification sur $r$ dans la première hypothèse. Je laisse ma version dans various.v le temps qu'on en discute. *)
-Lemma logn_prod [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
-  (forall n,  P n -> (0 < F n)%N) ->
-  (logn p (\prod_(n <- r | P n) F n) = \sum_(n <- r | P n) logn p (F n))%N.
-Proof.
-move=> F_gt0; elim/(big_load (fun n => (n > 0)%N)): _.
-elim/big_rec2: _; first by rewrite logn1.
-by move=> i m n Pi [n_gt0 <-]; rewrite muln_gt0 lognM ?F_gt0.
-Qed.
-
-End Temp.
diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index f899309..6a88026 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -175,18 +175,13 @@ apply/dvdn_partP => // p /[!(inE, mem_primes)]/and3P[p_prime _ pm].
 by rewrite p_part pfactor_dvdn// vp_le.
 Qed.
 
-Lemma logn_prod [I : eqType] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
-  {in r, forall n,  P n -> (0 < F n)%N} ->
+Lemma logn_prod [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
+  (forall n,  P n -> (0 < F n)%N) ->
   (logn p (\prod_(n <- r | P n) F n) = \sum_(n <- r | P n) logn p (F n))%N.
 Proof.
-elim: r => [|n r IHn Fnr0]; first by rewrite 2!big_nil logn1.
-have Fr0: {in r, forall n : I, P n -> (0 < F n)%N}.
-   by move=> i ir; apply/Fnr0; rewrite in_cons ir orbT.
-rewrite 2!big_cons; case /boolP: (P n) => Pn; last by apply/IHn.
-move: (Fnr0 n); rewrite mem_head Pn => /= /(_ is_true_true is_true_true) Fn0.
-rewrite lognM// ?IHn//.
-rewrite big_seq_cond big_mkcond prodn_gt0// => i.
-by case /boolP: ((i \in r) && P i) => // /andP[/Fr0].
+move=> F_gt0; elim/(big_load (fun n => (n > 0)%N)): _.
+elim/big_rec2: _; first by rewrite logn1.
+by move=> i m n Pi [n_gt0 <-]; rewrite muln_gt0 lognM ?F_gt0.
 Qed.
 
 Lemma logn_partn (p n : nat) (pi : nat_pred) :