remove backported lemmas to ssreflect

theories/xmathcomp/various.v

@@ -6,136 +6,6 @@
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-(*********************)
-(* package ssreflect *)
-(*********************)
-
-(***********)
-(* ssrbool *)
-(***********)
-
-Lemma classicPT (P : Type) : classically P <-> ((P -> False) -> False).
-Proof.
-split; first by move=>/(_ false) PFF PF; suff: false by []; apply: PFF => /PF.
-by move=> PFF []// Pf; suff: False by []; apply: PFF => /Pf.
-Qed.
-
-Lemma classic_sigW T (P : T -> Prop) :
-  classically (exists x, P x) <-> classically (sig P).
-Proof. by split; apply: classic_bind => -[x Px]; apply/classicW; exists x. Qed.
-
-Lemma classic_ex T (P : T -> Prop) :
-   ~ (forall x, ~ P x) -> classically (ex P).
-Proof.
-move=> NfNP; apply/classicPT => exPF; apply: NfNP => x Px.
-by apply: exPF; exists x.
-Qed.
-
-(*******)
-(* seq *)
-(*******)
-
-Lemma subset_mapP (X Y : eqType) (f : X -> Y) (s : seq X) (s' : seq Y) :
-    {subset s' <= map f s} <-> exists2 t, all (mem s) t & s' = map f t.
-Proof.
-split => [|[r /allP/= rE ->] _ /mapP[x xr ->]]; last by rewrite map_f ?rE.
-elim: s' => [|x s' IHs'] subss'; first by exists [::].
-have /mapP[y ys ->] := subss' _ (mem_head _ _).
-have [x' x's'|t st ->] := IHs'; first by rewrite subss'// inE x's' orbT.
-by exists (y :: t); rewrite //= ys st.
-Qed.
-Arguments subset_mapP {X Y}.
-
-(*********)
-(* bigop *)
-(*********)
-
-Lemma big_rcons_idx (R : Type) (idx : R) (op : R -> R -> R) (I : Type)
-    (i : I) (r : seq I) (P : pred I) (F : I -> R)
-    (idx' := if P i then op (F i) idx else idx) :
-  \big[op/idx]_(j <- rcons r i | P j) F j = \big[op/idx']_(j <- r | P j) F j.
-Proof. by elim: r => /= [|j r]; rewrite ?(big_nil, big_cons)// => ->. Qed.
-
-Lemma big_change_idx (R : Type) (idx : R) (op : Monoid.law idx) (I : Type)
-    (x : R)  (r : seq I) (P : pred I) (F : I -> R) :
-   op (\big[op/idx]_(j <- r | P j) F j) x = \big[op/x]_(j <- r | P j) F j.
-Proof.
-elim: r => [|i r]; rewrite ?(big_nil, big_cons, Monoid.mul1m)// => <-.
-by case: ifP => // Pi; rewrite Monoid.mulmA.
-Qed.
-Lemma big_rcons (R : Type) (idx : R) (op : Monoid.law idx) (I : Type)
-   i r (P : pred I) F :
-  \big[op/idx]_(j <- rcons r i | P j) F j =
-  op (\big[op/idx]_(j <- r | P j) F j) (if P i then F i else idx).
-Proof. by rewrite big_rcons_idx -big_change_idx Monoid.mulm1. Qed.
-
-(********)
-(* path *)
-(********)
-
-Lemma sortedP T x (s : seq T) (r : rel T) :
-  reflect (forall i, i.+1 < size s -> r (nth x s i) (nth x s i.+1)) (sorted r s).
-Proof.
-elim: s => [|y [|z s]//= IHs]/=; do ?by constructor.
-apply: (iffP andP) => [[ryz rzs] [|i]// /IHs->//|rS].
-by rewrite (rS 0); split=> //; apply/IHs => i /(rS i.+1).
-Qed.
-
-(*********)
-(* tuple *)
-(*********)
-
-Section tnth_shift.
-Context {T : Type} {n1 n2} (t1 : n1.-tuple T) (t2 : n2.-tuple T).
-
-Lemma tnth_lshift i : tnth [tuple of t1 ++ t2] (lshift n2 i) = tnth t1 i.
-Proof.
-have x0 := tnth_default t1 i; rewrite !(tnth_nth x0).
-by rewrite nth_cat size_tuple /= ltn_ord.
-Qed.
-
-Lemma tnth_rshift j : tnth [tuple of t1 ++ t2] (rshift n1 j) = tnth t2 j.
-Proof.
-have x0 := tnth_default t2 j; rewrite !(tnth_nth x0).
-by rewrite nth_cat size_tuple ltnNge leq_addr /= addKn.
-Qed.
-End tnth_shift.
-
-(*********)
-(* prime *)
-(*********)
-
-Lemma primeNsig (n : nat) : ~~ prime n -> (2 <= n)%N ->
-  { d : nat | (1 < d < n)%N & (d %| n)%N }.
-Proof.
-move=> primeN_n le2n; case/pdivP: {+}le2n => d /primeP[lt1d prime_d] dvd_dn.
-exists d => //; rewrite lt1d /= ltn_neqAle dvdn_leq 1?andbT //; last first.
-  by apply: (leq_trans _ le2n).
-by apply: contra primeN_n => /eqP <-; apply/primeP.
-Qed.
-
-Lemma totient_gt1 n : (totient n > 1)%N = (n > 2)%N.
-Proof.
-case: n => [|[|[|[|n']]]]//=; set n := n'.+4; rewrite [RHS]isT.
-have [pn2|/allPn[p]] := altP (@allP _ (eq_op^~ 2%N) (primes n)); last first.
-  rewrite mem_primes/=; move: p => [|[|[|p']]]//; set p := p'.+3.
-  move=> /andP[p_prime dvdkn].
-  have [//|[|k]// cpk ->] := (@pfactor_coprime _ n p_prime).
-  rewrite totient_coprime ?coprimeXr 1?coprime_sym//.
-  rewrite totient_pfactor ?logn_gt0 ?mem_primes ?p_prime// mulnCA.
-  by rewrite (@leq_trans p.-1) ?leq_pmulr ?muln_gt0 ?expn_gt0 ?totient_gt0.
-have pnNnil : primes n != [::].
-  apply: contraTneq isT => pn0.
-  by have := @prod_prime_decomp n isT; rewrite prime_decompE pn0/= big_nil.
-have := @prod_prime_decomp n isT; rewrite prime_decompE.
-case: (primes n) pnNnil pn2 (primes_uniq n) => [|p [|p' r]]//=; last first.
-  move=> _ eq2; rewrite !inE [p](eqP (eq2 _ _)) ?inE ?eqxx//.
-  by rewrite [p'](eqP (eq2 _ _)) ?inE ?eqxx// orbT.
-move=> _ /(_ _ (mem_head _ _))/eqP-> _; rewrite big_cons big_nil muln1/=.
-case: (logn 2 n) => [|[|k]]// ->.
-by rewrite totient_pfactor//= expnS mul1n leq_pmulr ?expn_gt0.
-Qed.
-
 (********************)
 (* package fingroup *)
 (********************)
@@ -635,7 +505,7 @@
   move=> WP; apply/subvP => u /(WP _ (fun=> 0)); rewrite big_nil; apply.
   by move=> i; rewrite mem0v.
 rewrite rcons_uniq => /andP[iNr r_uniq].
 apply: (iffP idP) => [+ u v uU vV|WP]; rewrite !big_rcons_idx.
   by move=> /IHr; apply => //; case: ifP => Pi//; rewrite memv_mul// vV.
 case: ifP => Pi; last first.
   by apply/IHr => // u v uU vV; have := WP _  _ uU vV; rewrite big_rcons_idx Pi.