Purge redundant misc lemmas (#61)

* forall_cons and exists_cons are available in MathComp 2.0, so remove local versions

* bigmax_seq_sup exists in MathComp 2.0 as bigmax_sup_seq, so remove local version

* card_leq_inj is leq_card and bij_card is bij_eq_card in MathComp 2.0, so remove local versions

theories/dfa.v

@@ -181,7 +181,7 @@ Section CutOff.
       case H: (size x < #|rT|.+1).
       + apply/existsP. exists (Ordinal H). apply/existsP. by exists (in_tuple x).
       + have: ~ injective (fun i : 'I_(size x) => f (take i x)).
-        { move/card_leq_inj. by rewrite -ltnS /= card_ord H. }
+        { move/leq_card. by rewrite -ltnS /= card_ord H. }
         move/injectiveP/injectivePn => [i [j]] Hij.
         wlog ltn_ij : i j {Hij} / i < j => [W|] E.
         { move: Hij. rewrite neq_ltn. case/orP => l; exact: W l _. }
@@ -429,7 +429,7 @@ Section NonRegular.
   Proof.
     move => f_spec [[A E]].
     pose f' (n : 'I_#|A|.+1) := delta_s A (f n).
-    suff: injective f' by move/card_leq_inj ; rewrite card_ord ltnn.
+    suff: injective f' by move/leq_card; rewrite card_ord ltnn.
     move => [n1 H1] [n2 H2]. rewrite /f' /delta_s /= => H.
     apply/eqP; change (n1 == n2); apply/eqP. apply: f_spec => w.
     by rewrite /residual !E !inE /dfa_accept !delta_cat H.
@@ -482,7 +482,7 @@ Section Pumping.
   Proof.
     rewrite -delta_lang => H1 H2.
     have/injectivePn : ~~ injectiveb (fun i : 'I_(size y) => delta (delta_s A x) (take i y)).
-      apply: contraL H2 => /injectiveP/card_leq_inj. by rewrite leqNgt card_ord.
+      apply: contraL H2 => /injectiveP/leq_card. by rewrite leqNgt card_ord.
     move => [i] [j] ij fij.
     wlog {ij} ij : i j fij / i < j. rewrite neq_ltn in ij. case/orP : ij => ij W; exact: W _ ij.
     exists (take i y), (sub i j y), (drop j y). split => [||k].

theories/minimization.v

@@ -68,7 +68,7 @@ Section Isomopism.
   Qed.
 
   Lemma dfa_iso_size : dfa_iso A B -> #|A| = #|B|.
-  Proof. move => [iso [H _ _ _]]. exact (bij_card H). Qed.
+  Proof. move => [iso [H _ _ _]]. exact (bij_eq_card H). Qed.
 End Isomopism.
 
 Lemma abstract_minimization A f :

theories/misc.v

@@ -56,22 +56,6 @@ Lemma index_take (T : eqType) (a : T) n (s : seq T) :
   a \in take n s -> index a (take n s) = index a s.
 Proof. move => H. by rewrite -{2}[s](cat_take_drop n) index_cat H. Qed.
 
-(* from mathcomp-1.13 *)
-Lemma forall_cons {T : eqType} {P : T -> Prop} {a s} :
-  {in a::s, forall x, P x} <-> P a /\ {in s, forall x, P x}.
-Proof.
-split=> [A|[A B]]; last by move => x /predU1P [-> //|]; apply: B.
-by split=> [|b Hb]; apply: A; rewrite !inE ?eqxx ?Hb ?orbT.
-Qed.
-
-(* from mathcomp-1.13 *)
-Lemma exists_cons {T : eqType} {P : T -> Prop} {a s} :
-  (exists2 x, x \in a::s & P x) <-> P a \/ exists2 x, x \in s & P x.
-Proof.
-split=> [[x /predU1P[->|x_s] Px]|]; [by left| by right; exists x|].
-by move=> [?|[x x_s ?]]; [exists a|exists x]; rewrite ?inE ?eqxx ?x_s ?orbT.
-Qed.
-
 Lemma orS (b1 b2 : bool) : b1 || b2 -> {b1} + {b2}.
 Proof. by case: b1 => /= [_|H]; [left|right]. Qed.
 
@@ -83,10 +67,6 @@ Proof.
   - rewrite inE. case/orS => [/eqP -> //|]. exact: B. 
 Qed.
 
-Lemma bigmax_seq_sup (T : eqType) (s:seq T) (P : pred T) F k m :
-  k \in s -> P k -> m <= F k -> m <= \max_(i <- s | P i) F i.
-Proof. move => A B C. by rewrite (big_rem k) //= B leq_max C. Qed.
-
 Lemma max_mem n0 (s : seq nat) : n0 \in s -> \max_(i <- s) i \in s.
 Proof. 
   case: s => // a s _. rewrite big_cons big_seq.
@@ -114,15 +94,6 @@ Lemma sub_exists (T : finType) (P1 P2 : pred T) :
   subpred P1 P2 -> [exists x, P1 x] -> [exists x, P2 x].
 Proof. move => H. case/existsP => x /H ?. apply/existsP. by exists x. Qed.
 
-Lemma card_leq_inj (T T' : finType) (f : T -> T') : injective f -> #|T| <= #|T'|.
-Proof. move => inj_f. by rewrite -(card_imset predT inj_f) max_card. Qed.
-
-Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.
-Proof.
-  case => g /can_inj Hf /can_inj Hg. apply/eqP.
-  by rewrite eqn_leq (card_leq_inj Hf) (card_leq_inj Hg).
-Qed.
-
 Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.
 Proof.
   move=> eq_pT; have [|g g1 g2 x] := @inj_card_bij (sig p) T _ val_inj.

theories/shepherdson.v

@@ -359,7 +359,7 @@ Section DFA2toAFA.
     apply: (@leq_trans #|{: table'}|); last by rewrite card_prod card_ffun !card_option expnS.
     pose f (x : image_type (@Tab_rc _ M)) : table' :=
       let (b,_) := x in ([pick q | q \in b.1],[ffun p => [pick q | (p,q) \in b.2]]).
-    suff : injective f by apply: card_leq_inj.
+    suff : injective f by apply: leq_card.
     move => [[a1 a2] Ha] [[b1 b2] Hb] [E1 /ffunP E2]. apply: val_inj => /=.
     move: Ha Hb => /dec_eq /= [x Hx] /dec_eq [y Hy].
     rewrite [Tab M x]surjective_pairing [Tab M y]surjective_pairing !xpair_eqE in Hx Hy.

theories/wmso.v

@@ -271,7 +271,7 @@ Proof.
   - rewrite I_of_glue0. case: (boolP (i < (\max_(k <- N) k).+1)) => ltn_max.
     + by rewrite (nth_map 0) ?size_iota // nth_iota.
     + rewrite nth_default ?size_map ?size_iota 1?leqNgt //.
-      apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_seq_sup H _ _.
+      apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_sup_seq H _ _.
   - rewrite I_of_glueS /= /I_of mem_filter mem_iota /= add0n.
     case: (ltnP i (size vs)) => H; first by rewrite andbT.
     rewrite andbF [nth _ _ i]nth_default //.
@@ -420,7 +420,7 @@ Proof.
           rewrite -addnS leq_add2l index_mem B andTb.
           rewrite nth_cat size_tk leqNgt leq_addr /= /i.
           by rewrite addnC -addnBA // subnn addn0 nth_index. }
-        have: i <= k by apply: bigmax_seq_sup i_in_X _ _.
+        have: i <= k by apply: bigmax_sup_seq i_in_X _ _.
         by rewrite /i addSn -ltn_subRL subnn.
     + move/hasPn => /= B. exists [::], v; split => // u in_v.
       apply/negbTE/negP => D.
@@ -457,7 +457,7 @@ Proof.
     by rewrite (nth_map (Ordinal lt_n)) ?size_enum_ord ?nth_enum_ord.
   + apply: contraNF A => A. rewrite ltnS. rewrite /lim.
     apply: bigmax_sup => //. instantiate (1 := Ordinal lt_n) => /=.
-    exact: bigmax_seq_sup A _ _ .
+    exact: bigmax_sup_seq A _ _ .
 Qed.
 
 Lemma vec_of_valP I s : satisfies I s <-> satisfies (I_of (vec_of_val I (bound s))) s.