diff options
Diffstat (limited to 'mathcomp')
34 files changed, 105 insertions, 104 deletions
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 28dd82b..dd3ce30 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -305,7 +305,7 @@ End FracField. Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)). Notation equivf := (@FracField.equivf _). -Hint Resolve denom_ratioP. +Hint Resolve denom_ratioP : core. Section Canonicals. diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 933bfcb..2f5e844 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -326,7 +326,7 @@ Proof. by rewrite !dvdzE abszM; apply: dvdn_mull. Qed. Lemma dvdz_mulr d m n : (d %| m)%Z -> (d %| m * n)%Z. Proof. by move=> d_m; rewrite mulrC dvdz_mull. Qed. -Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr. +Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr : core. Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2)%Z. Proof. by rewrite !dvdzE !abszM; apply: dvdn_mul. Qed. diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 1ca3414..b5d58cb 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -187,12 +187,12 @@ Proof. by move: bl br => [[] a|] [[] b|]. Qed. Lemma le_boundr_refl : reflexive le_boundr. Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed. -Hint Resolve le_boundr_refl. +Hint Resolve le_boundr_refl : core. Lemma le_boundl_refl : reflexive le_boundl. Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed. -Hint Resolve le_boundl_refl. +Hint Resolve le_boundl_refl : core. Lemma le_boundl_bb x b1 b2 : le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2). @@ -242,7 +242,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //; | by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)]. Qed. -Hint Rewrite intP. +Hint Rewrite intP : core. Arguments itvP [x i]. Definition subitv (i1 i2 : interval R) := diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index a8a91d3..7875b83 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -388,7 +388,7 @@ case: GaussE (IHm _ B) => [[L U] r] /= uL. rewrite unitmxE xrowE det_mulmx (@det_lblock _ 1) det1 mul1r unitrM. by rewrite -unitmxE unitmx_perm. Qed. -Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit. +Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit : core. Lemma mulmx_ebase m n (A : 'M_(m, n)) : col_ebase A *m pid_mx (\rank A) *m row_ebase A = A. @@ -504,7 +504,7 @@ Arguments submxP {m1 m2 n A B}. Lemma submx_refl m n (A : 'M_(m, n)) : (A <= A)%MS. Proof. by rewrite submxE mulmx_coker. Qed. -Hint Resolve submx_refl. +Hint Resolve submx_refl : core. Lemma submxMl m n p (D : 'M_(m, n)) (A : 'M_(n, p)) : (D *m A <= A)%MS. Proof. by rewrite submxE -mulmxA mulmx_coker mulmx0. Qed. @@ -874,7 +874,7 @@ Proof. apply/row_fullP; exists (pid_mx (\rank A) *m invmx (col_ebase A)). by rewrite !mulmxA mulmxKV // pid_mx_id // pid_mx_1. Qed. -Hint Resolve row_base_free col_base_full. +Hint Resolve row_base_free col_base_full : core. Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A <= B)%MS -> \rank A <= \rank B ?= iff (B <= A)%MS. @@ -1974,7 +1974,7 @@ End Eigenspace. End RowSpaceTheory. -Hint Resolve submx_refl. +Hint Resolve submx_refl : core. Arguments submxP {F m1 m2 n A B}. Arguments eq_row_sub [F m n v A]. Arguments row_subP {F m1 m2 n A B}. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index fe5de6d..f679828 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -899,7 +899,7 @@ apply: integral_horner_root mon_p pu0 intRp _. by apply/integral_poly => i; rewrite coefX; apply: integral_nat. Qed. -Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K). +Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K) : core. Let XsubC0 (u : K) : root ('X - u%:P) u. Proof. by rewrite root_XsubC. Qed. Let intR_XsubC u : diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 34b6e7b..026af3d 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -868,7 +868,7 @@ case: (eqVneq q 0) => [->|nzq]; last by rewrite expf_neq0 ?lead_coef_eq0. by rewrite /scalp 2!unlock /= eqxx lead_coef0 unitr0 /= oner_neq0. Qed. -Hint Resolve lc_expn_scalp_neq0. +Hint Resolve lc_expn_scalp_neq0 : core. Variant edivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> bool -> Type := @@ -988,7 +988,7 @@ Qed. End WeakTheoryForIDomainPseudoDivision. -Hint Resolve lc_expn_scalp_neq0. +Hint Resolve lc_expn_scalp_neq0 : core. End WeakIdomain. @@ -1049,7 +1049,7 @@ Proof. by rewrite /modp unlock redivp_def /=; case: ifP; rewrite rmodp1 // scaler0. Qed. -Hint Resolve divp0 divp1 mod0p modp0 modp1. +Hint Resolve divp0 divp1 mod0p modp0 modp1 : core. Lemma modp_small p q : size p < size q -> p %% q = p. Proof. @@ -1156,7 +1156,7 @@ Qed. Lemma dvdp0 d : d %| 0. Proof. by rewrite /dvdp mod0p. Qed. -Hint Resolve dvdp0. +Hint Resolve dvdp0 : core. Lemma dvd0p p : (0 %| p) = (p == 0). Proof. by rewrite /dvdp modp0. Qed. @@ -1231,7 +1231,7 @@ Qed. Lemma dvdpp d : d %| d. Proof. by rewrite /dvdp modpp. Qed. -Hint Resolve dvdpp. +Hint Resolve dvdpp : core. Lemma divp_dvd p q : (p %| q) -> ((q %/ p) %| q). Proof. @@ -1253,7 +1253,7 @@ Qed. Lemma dvdp_mulr n d m : d %| m -> d %| m * n. Proof. by move=> hdm; rewrite mulrC dvdp_mull. Qed. -Hint Resolve dvdp_mull dvdp_mulr. +Hint Resolve dvdp_mull dvdp_mulr : core. Lemma dvdp_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2. Proof. @@ -1468,7 +1468,7 @@ Qed. Lemma eqpxx : reflexive (@eqp R). Proof. by move=> p; rewrite /eqp dvdpp. Qed. -Hint Resolve eqpxx. +Hint Resolve eqpxx : core. Lemma eqp_sym : symmetric (@eqp R). Proof. by move=> p q; rewrite /eqp andbC. Qed. @@ -2533,8 +2533,8 @@ Qed. End IDomainPseudoDivision. -Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp. -Hint Resolve dvdp0. +Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core. +Hint Resolve dvdp0 : core. End CommonIdomain. diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 6015f33..14fde5a 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -56,7 +56,7 @@ Definition denq x := nosimpl ((valq x).2). Lemma denq_gt0 x : 0 < denq x. Proof. by rewrite /denq; case: x=> [[a b] /= /andP []]. Qed. -Hint Resolve denq_gt0. +Hint Resolve denq_gt0 : core. Definition denq_ge0 x := ltrW (denq_gt0 x). @@ -64,7 +64,7 @@ Lemma denq_lt0 x : (denq x < 0) = false. Proof. by rewrite ltr_gtF. Qed. Lemma denq_neq0 x : denq x != 0. Proof. by rewrite /denq gtr_eqF ?denq_gt0. Qed. -Hint Resolve denq_neq0. +Hint Resolve denq_neq0 : core. Lemma denq_eq0 x : (denq x == 0) = false. Proof. exact: negPf (denq_neq0 _). Qed. @@ -368,7 +368,7 @@ Qed. Notation "n %:Q" := ((n : int)%:~R : rat) (at level 2, left associativity, format "n %:Q") : ring_scope. -Hint Resolve denq_neq0 denq_gt0 denq_ge0. +Hint Resolve denq_neq0 denq_gt0 denq_ge0 : core. Definition subq (x y : rat) : rat := (addq x (oppq y)). Definition divq (x y : rat) : rat := (mulq x (invq y)). diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 5542959..40a1f83 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1305,7 +1305,7 @@ Hypothesis charFp : p \in [char R]. Lemma charf0 : p%:R = 0 :> R. Proof. by apply/eqP; case/andP: charFp. Qed. Lemma charf_prime : prime p. Proof. by case/andP: charFp. Qed. -Hint Resolve charf_prime. +Hint Resolve charf_prime : core. Lemma mulrn_char x : x *+ p = 0. Proof. by rewrite -mulr_natl charf0 mul0r. Qed. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 614fbc2..b734ad7 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -967,7 +967,7 @@ Proof. by rewrite mulrz_eq0 negb_or. Qed. Lemma realz n : (n%:~R : R) \in Num.real. Proof. by rewrite -topredE /Num.real /= ler0z lerz0 ler_total. Qed. -Hint Resolve realz. +Hint Resolve realz : core. Definition intr_inj := @mulrIz 1 (oner_neq0 R). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index ae0c00b..2414e13 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1045,7 +1045,7 @@ Lemma realE x : (x \is real) = (0 <= x) || (x <= 0). Proof. by []. Qed. Lemma lerr x : x <= x. Proof. exact: lerr. Qed. Lemma ltrr x : x < x = false. Proof. by rewrite ltr_def eqxx. Qed. Lemma ltrW x y : x < y -> x <= y. Proof. exact: ltrW. Qed. -Hint Resolve lerr ltrr ltrW. +Hint Resolve lerr ltrr ltrW : core. Lemma ltr_neqAle x y : (x < y) = (x != y) && (x <= y). Proof. by rewrite ltr_def eq_sym. Qed. @@ -1080,12 +1080,12 @@ Qed. Lemma ler01 : 0 <= 1 :> R. Proof. exact: ler01. Qed. Lemma ltr01 : 0 < 1 :> R. Proof. exact: ltr01. Qed. Lemma ler0n n : 0 <= n%:R :> R. Proof. by rewrite -nnegrE rpred_nat. Qed. -Hint Resolve ler01 ltr01 ler0n. +Hint Resolve ler01 ltr01 ler0n : core. Lemma ltr0Sn n : 0 < n.+1%:R :> R. Proof. by elim: n => // n; apply: addr_gt0. Qed. Lemma ltr0n n : (0 < n%:R :> R) = (0 < n)%N. Proof. by case: n => //= n; apply: ltr0Sn. Qed. -Hint Resolve ltr0Sn. +Hint Resolve ltr0Sn : core. Lemma pnatr_eq0 n : (n%:R == 0 :> R) = (n == 0)%N. Proof. by case: n => [|n]; rewrite ?mulr0n ?eqxx // gtr_eqF. Qed. @@ -1154,7 +1154,7 @@ by rewrite -{2}normrN -normr0 -(subrr x) ler_norm_add. Qed. Lemma normr_ge0 x : 0 <= `|x|. Proof. by rewrite ger0_def normr_id. Qed. -Hint Resolve normr_ge0. +Hint Resolve normr_ge0 : core. Lemma ler0_norm x : x <= 0 -> `|x| = - x. Proof. by move=> x_le0; rewrite -[r in _ = r]ger0_norm ?normrN ?oppr_ge0. Qed. @@ -1263,7 +1263,7 @@ Arguments ltr01 {R}. Arguments normr_idP {R x}. Arguments normr0P {R x}. Arguments lerifP {R x y C}. -Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0. +Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0 : core. Section NumIntegralDomainMonotonyTheory. @@ -1450,10 +1450,10 @@ Implicit Types x y z t : R. Lemma ler_opp2 : {mono -%R : x y /~ x <= y :> R}. Proof. by move=> x y /=; rewrite -subr_ge0 opprK addrC subr_ge0. Qed. -Hint Resolve ler_opp2. +Hint Resolve ler_opp2 : core. Lemma ltr_opp2 : {mono -%R : x y /~ x < y :> R}. Proof. by move=> x y /=; rewrite lerW_nmono. Qed. -Hint Resolve ltr_opp2. +Hint Resolve ltr_opp2 : core. Definition lter_opp2 := (ler_opp2, ltr_opp2). Lemma ler_oppr x y : (x <= - y) = (y <= - x). @@ -1525,10 +1525,10 @@ Lemma ltr0_real x : x < 0 -> x \is real. Proof. by move=> /ltrW/ler0_real. Qed. Lemma real0 : 0 \is @real R. Proof. by rewrite ger0_real. Qed. -Hint Resolve real0. +Hint Resolve real0 : core. Lemma real1 : 1 \is @real R. Proof. by rewrite ger0_real. Qed. -Hint Resolve real1. +Hint Resolve real1 : core. Lemma realn n : n%:R \is @real R. Proof. by rewrite ger0_real. Qed. @@ -2640,7 +2640,7 @@ Qed. (* norm + add *) Lemma normr_real x : `|x| \is real. Proof. by rewrite ger0_real. Qed. -Hint Resolve normr_real. +Hint Resolve normr_real : core. Lemma ler_norm_sum I r (G : I -> R) (P : pred I): `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i|. @@ -3144,7 +3144,7 @@ Qed. End NumDomainOperationTheory. -Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real. +Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real : core. Arguments ler_sqr {R} [x y]. Arguments ltr_sqr {R} [x y]. Arguments signr_inj {R} [x1 x2]. @@ -3429,13 +3429,13 @@ End NumFieldTheory. Section RealDomainTheory. -Hint Resolve lerr. +Hint Resolve lerr : core. Variable R : realDomainType. Implicit Types x y z t : R. Lemma num_real x : x \is real. Proof. exact: num_real. Qed. -Hint Resolve num_real. +Hint Resolve num_real : core. Lemma ler_total : total (@le R). Proof. by move=> x y; apply: real_leVge. Qed. @@ -3534,14 +3534,14 @@ Proof. by rewrite -real_normrEsign. Qed. End RealDomainTheory. -Hint Resolve num_real. +Hint Resolve num_real : core. Section RealDomainMonotony. Variables (R : realDomainType) (R' : numDomainType) (D : pred R) (f : R -> R'). Implicit Types (m n p : nat) (x y z : R) (u v w : R'). -Hint Resolve (@num_real R). +Hint Resolve (@num_real R) : core. Lemma homo_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}. Proof. by move=> mf x y; apply: real_mono. Qed. @@ -3569,7 +3569,7 @@ Section RealDomainOperations. Variable R : realDomainType. Implicit Types x y z t : R. -Hint Resolve (@num_real R). +Hint Resolve (@num_real R) : core. Lemma sgr_cp0 x : ((sg x == 1) = (0 < x)) * @@ -4032,7 +4032,7 @@ Lemma poly_ivt : real_closed_axiom R. Proof. exact: poly_ivt. Qed. Lemma sqrtr_ge0 a : 0 <= sqrt a. Proof. by rewrite /sqrt; case: (sig2W _). Qed. -Hint Resolve sqrtr_ge0. +Hint Resolve sqrtr_ge0 : core. Lemma sqr_sqrtr a : 0 <= a -> sqrt a ^+ 2 = a. Proof. @@ -4325,7 +4325,7 @@ Proof. rewrite CrealE fmorph_div rmorph_nat rmorphM rmorphB conjCK. by rewrite conjCi -opprB mulrNN. Qed. -Hint Resolve Creal_Re Creal_Im. +Hint Resolve Creal_Re Creal_Im : core. Fact Re_is_additive : additive Re. Proof. by move=> x y; rewrite /Re rmorphB addrACA -opprD mulrBl. Qed. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 75b2073..c4c62c3 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -460,7 +460,7 @@ by have:= sU12 (r2v u); rewrite !memvE /subsetv !genmxE r2vK. Qed. Lemma subvv U : (U <= U)%VS. Proof. exact/subvP. Qed. -Hint Resolve subvv. +Hint Resolve subvv : core. Lemma subv_trans : transitive subV. Proof. by move=> U V W /subvP sUV /subvP sVW; apply/subvP=> u /sUV/sVW. Qed. @@ -1222,7 +1222,7 @@ End BigSumBasis. End VectorTheory. -Hint Resolve subvv. +Hint Resolve subvv : core. Arguments subvP {K vT U V}. Arguments addv_idPl {K vT U V}. Arguments addv_idPr {K vT U V}. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index a657fa5..9a61ebe 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -576,7 +576,7 @@ Proof. by move=> i; rewrite /irr_of_socle enum_valK cast_ordK addrK. Qed. Lemma irr_of_socleK : cancel irr_of_socle W. Proof. by move=> Wi; rewrite /W subrK cast_ordKV enum_rankK. Qed. -Hint Resolve socle_of_IirrK irr_of_socleK. +Hint Resolve socle_of_IirrK irr_of_socleK : core. Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}. Proof. by apply: onW_bij; exists W. Qed. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 7b2b90d..a4ecd2c 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -759,7 +759,7 @@ Arguments classfun_on {gT} B%g A%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. Arguments cfun_onP {gT G A phi}. -Hint Resolve cfun_onT. +Hint Resolve cfun_onT : core. Section DotProduct. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 69055d4..22ab389 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -511,7 +511,7 @@ Proof. by rewrite im_abelem_rV inE. Qed. Lemma sub_im_abelem_rV mA : subset mA (mem (ErV @* E)). Proof. by rewrite unlock; apply/pred0P=> v /=; rewrite mem_im_abelem_rV. Qed. -Hint Resolve mem_im_abelem_rV sub_im_abelem_rV. +Hint Resolve mem_im_abelem_rV sub_im_abelem_rV : core. Lemma abelem_rV_1 : ErV 1 = 0%R. Proof. by rewrite morph1. Qed. @@ -552,7 +552,7 @@ Proof. by rewrite -im_rVabelem mem_morphim. Qed. Lemma sub_rVabelem L : rV_E @* L \subset E. Proof. by rewrite -[_ @* L]morphimIim im_invm subsetIl. Qed. -Hint Resolve mem_rVabelem sub_rVabelem. +Hint Resolve mem_rVabelem sub_rVabelem : core. Lemma card_rVabelem L : #|rV_E @* L| = #|L|. Proof. by rewrite card_injm ?rVabelem_injm. Qed. diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 4b37a9c..fc01763 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -607,7 +607,7 @@ Local Notation intrp := (map_poly intr). Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC). +Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. (* Specialization of a few basic ssrnum order lemmas. *) @@ -645,7 +645,8 @@ Definition algC_algebraic x := Algebraics.Implementation.algebraic x. Lemma Creal0 : 0 \is Creal. Proof. exact: rpred0. Qed. Lemma Creal1 : 1 \is Creal. Proof. exact: rpred1. Qed. -Hint Resolve Creal0 Creal1. (* Trivial cannot resolve a general real0 hint. *) +(* Trivial cannot resolve a general real0 hint. *) +Hint Resolve Creal0 Creal1 : core. Lemma algCrect x : x = 'Re x + 'i * 'Im x. Proof. by rewrite [LHS]Crect. Qed. @@ -655,7 +656,7 @@ Proof. by rewrite Creal_Re. Qed. Lemma algCreal_Im x : 'Im x \is Creal. Proof. by rewrite Creal_Im. Qed. -Hint Resolve algCreal_Re algCreal_Im. +Hint Resolve algCreal_Re algCreal_Im : core. (* Integer subset. *) (* Not relying on the undocumented interval library, for now. *) @@ -680,7 +681,7 @@ Lemma floorCK : {in Cint, cancel floorC intr}. Proof. by move=> z /eqP. Qed. Lemma floorC0 : floorC 0 = 0. Proof. exact: (intCK 0). Qed. Lemma floorC1 : floorC 1 = 1. Proof. exact: (intCK 1). Qed. -Hint Resolve floorC0 floorC1. +Hint Resolve floorC0 floorC1 : core. Lemma floorCpK (p : {poly algC}) : p \is a polyOver Cint -> map_poly intr (map_poly floorC p) = p. @@ -723,7 +724,7 @@ Proof. by case/CintP=> m ->; apply: rpred_int. Qed. Lemma Cint0 : 0 \in Cint. Proof. exact: (Cint_int 0). Qed. Lemma Cint1 : 1 \in Cint. Proof. exact: (Cint_int 1). Qed. -Hint Resolve Cint0 Cint1. +Hint Resolve Cint0 Cint1 : core. Fact Cint_key : pred_key Cint. Proof. by []. Qed. Fact Cint_subring : subring_closed Cint. @@ -814,7 +815,7 @@ Proof. by case/CnatP=> n ->; apply: rpred_nat. Qed. Lemma Cnat_nat n : n%:R \in Cnat. Proof. by apply/CnatP; exists n. Qed. Lemma Cnat0 : 0 \in Cnat. Proof. exact: (Cnat_nat 0). Qed. Lemma Cnat1 : 1 \in Cnat. Proof. exact: (Cnat_nat 1). Qed. -Hint Resolve Cnat_nat Cnat0 Cnat1. +Hint Resolve Cnat_nat Cnat0 Cnat1 : core. Fact Cnat_key : pred_key Cnat. Proof. by []. Qed. Fact Cnat_semiring : semiring_closed Cnat. @@ -970,7 +971,7 @@ Proof. by move=> x_dv_y /dvdCP[m Zm ->]; apply: dvdC_mull. Qed. Lemma dvdC_refl x : (x %| x)%C. Proof. by apply/dvdCP; exists 1; rewrite ?mul1r. Qed. -Hint Resolve dvdC_refl. +Hint Resolve dvdC_refl : core. Fact dvdC_key x : pred_key (dvdC x). Proof. by []. Qed. Lemma dvdC_zmod x : zmod_closed (dvdC x). @@ -1004,7 +1005,7 @@ Lemma eqCmod_refl e x : (x == x %[mod e])%C. Proof. by rewrite /eqCmod subrr rpred0. Qed. Lemma eqCmodm0 e : (e == 0 %[mod e])%C. Proof. by rewrite /eqCmod subr0. Qed. -Hint Resolve eqCmod_refl eqCmodm0. +Hint Resolve eqCmod_refl eqCmodm0 : core. Lemma eqCmod0 e x : (x == 0 %[mod e])%C = (e %| x)%C. Proof. by rewrite /eqCmod subr0. Qed. @@ -1091,7 +1092,7 @@ Qed. Lemma Crat0 : 0 \in Crat. Proof. by apply/CratP; exists 0; rewrite rmorph0. Qed. Lemma Crat1 : 1 \in Crat. Proof. by apply/CratP; exists 1; rewrite rmorph1. Qed. -Hint Resolve Crat0 Crat1. +Hint Resolve Crat0 Crat1 : core. Fact Crat_key : pred_key Crat. Proof. by []. Qed. Fact Crat_divring_closed : divring_closed Crat. @@ -1236,5 +1237,5 @@ Proof. by move=> _ u /CintP[m ->]; apply: rpredZint. Qed. End PredCmod. End AlgebraicsTheory. -Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1. -Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0. +Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1 : core. +Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 5d78cac..1db4aa4 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -56,7 +56,7 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC). +Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. Local Notation QtoCm := [rmorphism of QtoC]. (* Number fields and rational spans. *) @@ -550,7 +550,7 @@ Proof. by rewrite Aint_Cint ?Cint_int. Qed. Lemma Aint0 : 0 \in Aint. Proof. exact: (Aint_int 0). Qed. Lemma Aint1 : 1 \in Aint. Proof. exact: (Aint_int 1). Qed. -Hint Resolve Aint0 Aint1. +Hint Resolve Aint0 Aint1 : core. Lemma Aint_unity_root n x : (n > 0)%N -> n.-unity_root x -> x \in Aint. Proof. @@ -702,7 +702,7 @@ Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope. Lemma eqAmod_refl e x : (x == x %[mod e])%A. Proof. by rewrite /eqAmod subrr rpred0. Qed. -Hint Resolve eqAmod_refl. +Hint Resolve eqAmod_refl : core. Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A. Proof. by rewrite /eqAmod -opprB rpredN. Qed. @@ -739,7 +739,7 @@ Qed. Lemma eqAmodm0 e : (e == 0 %[mod e])%A. Proof. by rewrite /eqAmod subr0 unfold_in; case: ifPn => // /divff->. Qed. -Hint Resolve eqAmodm0. +Hint Resolve eqAmodm0 : core. Lemma eqAmodMr e : {in Aint, forall z x y, x == y %[mod e] -> x * z == y * z %[mod e]}%A. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 009c1ae..76039d1 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -95,7 +95,7 @@ Definition qf_cps T D (x : cps T) := Lemma qf_cps_ret T D (x : T) : D x -> qf_cps D (ret x). Proof. move=> ??; exact. Qed. -Hint Resolve qf_cps_ret. +Hint Resolve qf_cps_ret : core. Lemma qf_cps_bind T1 D1 T2 D2 (x : cps T1) (f : T1 -> cps T2) : qf_cps D1 x -> (forall x, D1 x -> qf_cps D2 (f x)) -> qf_cps D2 (bind x f). diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 80bdf50..afb0b0b 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -122,7 +122,7 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj [numDomainType of algC]). +Local Hint Resolve (@intr_inj [numDomainType of algC]) : core. Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]). Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 320331c..5f28b7d 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -449,7 +449,7 @@ End Characteristicity. Arguments characteristic _ _%g _%g. Notation "H \char G" := (characteristic H G) : group_scope. -Hint Resolve char_refl. +Hint Resolve char_refl : core. Section InjmChar. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 19cefcd..f436102 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -492,7 +492,7 @@ Qed. End PreGroupIdentities. -Hint Resolve commute1. +Hint Resolve commute1 : core. Arguments invg_inj {T} [x1 x2]. Prenex Implicits commute invgK. @@ -1358,7 +1358,7 @@ Lemma valG : val G = G. Proof. by []. Qed. (* Non-triviality. *) Lemma group1 : 1 \in G. Proof. by case/group_setP: (valP G). Qed. -Hint Resolve group1. +Hint Resolve group1 : core. (* Loads of silly variants to placate the incompleteness of trivial. *) (* An alternative would be to upgrade done, pending better support *) @@ -1647,7 +1647,7 @@ Proof. by move=> y Gy /=; rewrite -class_rcoset rcoset_id. Qed. Lemma class_refl x : x \in x ^: G. Proof. by apply/imsetP; exists 1; rewrite ?conjg1. Qed. -Hint Resolve class_refl. +Hint Resolve class_refl : core. Lemma class_eqP x y : reflect (x ^: G = y ^: G) (x \in y ^: G). Proof. @@ -1794,7 +1794,7 @@ Proof. by move=> x y Gx Gy; apply: val_inj; rewrite /= !subgK ?groupM. Qed. End OneGroup. -Hint Resolve group1. +Hint Resolve group1 : core. Lemma groupD1_inj G H : G^# = H^# -> G :=: H. Proof. by move/(congr1 (setU 1)); rewrite !setD1K. Qed. @@ -1842,9 +1842,9 @@ Qed. End GroupProp. -Hint Resolve group1 group1_class1 group1_class12 group1_class12. -Hint Resolve group1_eqType group1_finType. -Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0. +Hint Resolve group1 group1_class1 group1_class12 group1_class12 : core. +Hint Resolve group1_eqType group1_finType : core. +Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0 : core. Notation "G :^ x" := (conjG_group G x) : Group_scope. @@ -1907,7 +1907,7 @@ Proof. exact: cardG_gt0. Qed. End GroupInter. -Hint Resolve order_gt0. +Hint Resolve order_gt0 : core. Arguments generated_group _ _%g. Arguments joing_group _ _%g _%g. @@ -3005,7 +3005,7 @@ Notation "''C_' G [ x ]" := (setI_group G 'C[x]) : Group_scope. Notation "''C_' ( G ) [ x ]" := (setI_group G 'C[x]) (only parsing) : Group_scope. -Hint Resolve normG normal_refl. +Hint Resolve normG normal_refl : core. Section MinMaxGroup. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 4b2d863..cb02991 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -1495,7 +1495,7 @@ Proof. by apply/injmP; apply: in2W; apply: subg_inj. Qed. Lemma injm_subg : 'injm (subg G). Proof. by apply/injmP; apply: can_in_inj (@subgK _ _). Qed. -Hint Resolve injm_sgval injm_subg. +Hint Resolve injm_sgval injm_subg : core. Lemma ker_sgval : 'ker sgval = 1. Proof. exact/trivgP. Qed. Lemma ker_subg : 'ker (subg G) = 1. Proof. exact/trivgP. Qed. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 01ef08e..b1a7dd7 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -129,7 +129,7 @@ Lemma perm_inj s : injective s. Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. Arguments perm_inj : clear implicits. -Hint Resolve perm_inj. +Hint Resolve perm_inj : core. Lemma perm_onto s : codom s =i predT. Proof. by apply/subset_cardP; rewrite ?card_codom ?subset_predT. Qed. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 746898f..16ce432 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -249,7 +249,7 @@ Proof. by apply/dvdn_biglcmP=> x Gx; apply: order_dvdG. Qed. Lemma exponent_gt0 G : 0 < exponent G. Proof. exact: dvdn_gt0 (exponent_dvdn G). Qed. -Hint Resolve exponent_gt0. +Hint Resolve exponent_gt0 : core. Lemma pnat_exponent pi G : pi.-nat (exponent G) = pi.-group G. Proof. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 88774db..e2c6f48 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -375,7 +375,7 @@ rewrite /cpairg1 /cpair1g; do 2!case: restrmP => _ [_ _ _ -> //]. rewrite !morphim_comp morphim_cents // morphim_pair1g morphim_pairg1. by case/dprodP: (setX_dprod H K). Qed. -Hint Resolve im_cpair_cent. +Hint Resolve im_cpair_cent : core. Lemma im_cpair : CH * CK = C. Proof. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 2db8927..f108ff9 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -558,7 +558,7 @@ Qed. Lemma mem_index_enum T i : i \in index_enum T. Proof. by rewrite -[index_enum T]enumT mem_enum. Qed. -Hint Resolve mem_index_enum. +Hint Resolve mem_index_enum : core. Lemma filter_index_enum T P : filter P (index_enum T) = enum P. Proof. by []. Qed. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index ed1eedf..80c9312 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -327,7 +327,7 @@ Proof. by case/dvdnP=> n' ->; rewrite /dvdn mulnA modnMl. Qed. Lemma dvdn_mulr d m n : d %| m -> d %| m * n. Proof. by move=> d_m; rewrite mulnC dvdn_mull. Qed. -Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr. +Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr : core. Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2. Proof. @@ -462,7 +462,7 @@ case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt. by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull]. Qed. -Hint Resolve dvdn_add dvdn_sub dvdn_exp. +Hint Resolve dvdn_add dvdn_sub dvdn_exp : core. Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n). Proof. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 6ed4b97..dc3daf0 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -196,7 +196,7 @@ Notation eqxx := eq_refl. Lemma eq_sym (T : eqType) (x y : T) : (x == y) = (y == x). Proof. exact/eqP/eqP. Qed. -Hint Resolve eq_refl eq_sym. +Hint Resolve eq_refl eq_sym : core. Section Contrapositives. diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index c534b7b..5358dc7 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -216,7 +216,7 @@ Definition closure_mem m_a : pred T := End Connect. -Hint Resolve connect0. +Hint Resolve connect0 : core. Notation n_comp e a := (n_comp_mem e (mem a)). Notation closed e a := (closed_mem e (mem a)). diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 4ad02c6..9ca96c8 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -244,7 +244,7 @@ End BasicSetTheory. Definition inE := (in_set, inE). Arguments set0 {T}. -Hint Resolve in_setT. +Hint Resolve in_setT : core. Notation "[ 'set' : T ]" := (setTfor (Phant T)) (at level 0, format "[ 'set' : T ]") : set_scope. @@ -348,7 +348,7 @@ Proof. by apply/subsetP=> x; rewrite inE. Qed. Lemma subsetT_hint mA : subset mA (mem [set: T]). Proof. by rewrite unlock; apply/pred0P=> x; rewrite !inE. Qed. -Hint Resolve subsetT_hint. +Hint Resolve subsetT_hint : core. Lemma subTset A : (setT \subset A) = (A == setT). Proof. by rewrite eqEsubset subsetT. Qed. @@ -975,7 +975,7 @@ Arguments subUsetP {T A B C}. Arguments subsetDP {T A B C}. Arguments subsetD1P {T A B x}. Prenex Implicits set1. -Hint Resolve subsetT_hint. +Hint Resolve subsetT_hint : core. Section setOpsAlgebra. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 8be2eb0..441fc12 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -626,7 +626,7 @@ Lemma subxx_hint (mA : mem_pred T) : subset mA mA. Proof. by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->. Qed. -Hint Resolve subxx_hint. +Hint Resolve subxx_hint : core. (* The parametrization by predType makes it easier to apply subxx. *) Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA. @@ -818,7 +818,7 @@ Proof. by rewrite !disjoint_has has_cat negb_or. Qed. End OpsTheory. -Hint Resolve subxx_hint. +Hint Resolve subxx_hint : core. Arguments pred0P {T P}. Arguments pred0Pn {T P}. @@ -1585,7 +1585,7 @@ End OrdinalSub. Notation "''I_' n" := (ordinal n) (at level 8, n at level 2, format "''I_' n"). -Hint Resolve ltn_ord. +Hint Resolve ltn_ord : core. Section OrdinalEnum. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index f30c3a1..b7a8444 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -491,7 +491,7 @@ Proof. by apply: right_trans; [apply: equiv_sym|apply: equiv_trans]. Qed. End EquivRel. -Hint Resolve equiv_refl. +Hint Resolve equiv_refl : core. Notation EquivRel r er es et := (@EquivRelPack _ r (EquivClass er es et)). Notation "[ 'equiv_rel' 'of' e ]" := (@equiv_pack _ _ e _ id) diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 02064c3..2a07d17 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -358,7 +358,7 @@ Proof. by case/primeP. Qed. Lemma prime_gt0 p : prime p -> 0 < p. Proof. by move/prime_gt1; apply: ltnW. Qed. -Hint Resolve prime_gt1 prime_gt0. +Hint Resolve prime_gt1 prime_gt0 : core. Lemma prod_prime_decomp n : n > 0 -> n = \prod_(f <- prime_decomp n) f.1 ^ f.2. @@ -494,7 +494,7 @@ Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?pdiv_prime. Qed. Lemma max_pdiv_gt0 n : 0 < max_pdiv n. Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?max_pdiv_prime. Qed. -Hint Resolve pdiv_gt0 max_pdiv_gt0. +Hint Resolve pdiv_gt0 max_pdiv_gt0 : core. Lemma pdiv_min_dvd m d : 1 < d -> d %| m -> pdiv m <= d. Proof. @@ -636,7 +636,7 @@ Proof. by rewrite lognE dvdn1 /= andbC; case: eqP => // ->. Qed. Lemma pfactor_gt0 p n : 0 < p ^ logn p n. Proof. by rewrite expn_gt0 lognE; case: (posnP p) => // ->. Qed. -Hint Resolve pfactor_gt0. +Hint Resolve pfactor_gt0 : core. Lemma pfactor_dvdn p n m : prime p -> m > 0 -> (p ^ n %| m) = (n <= logn p m). Proof. @@ -858,7 +858,7 @@ Qed. Lemma part_gt0 pi n : 0 < n`_pi. Proof. exact: prodn_gt0. Qed. -Hint Resolve part_gt0. +Hint Resolve part_gt0 : core. Lemma sub_in_partn pi1 pi2 n : {in \pi(n), {subset pi1 <= pi2}} -> n`_pi1 %| n`_pi2. @@ -1219,7 +1219,7 @@ Lemma odd_2'nat n : odd n = 2^'.-nat n. Proof. by case: n => // n; rewrite p'natE // dvdn2 negbK. Qed. End PnatTheory. -Hint Resolve part_gt0. +Hint Resolve part_gt0 : core. (************************************) (* Properties of the divisors list. *) diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index ba1f969..2c9fd64 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1422,7 +1422,7 @@ Qed. Lemma perm_eq_refl s : perm_eq s s. Proof. exact/perm_eqP. Qed. -Hint Resolve perm_eq_refl. +Hint Resolve perm_eq_refl : core. Lemma perm_eq_sym : symmetric perm_eq. Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed. @@ -1601,7 +1601,7 @@ Arguments perm_eqP {T s1 s2}. Arguments perm_eqlP {T s1 s2}. Arguments perm_eqrP {T s1 s2}. Prenex Implicits perm_eq. -Hint Resolve perm_eq_refl. +Hint Resolve perm_eq_refl : core. Section RotrLemmas. @@ -1827,7 +1827,7 @@ Qed. Lemma subseq_refl s : subseq s s. Proof. by elim: s => //= x s IHs; rewrite eqxx. Qed. -Hint Resolve subseq_refl. +Hint Resolve subseq_refl : core. Lemma cat_subseq s1 s2 s3 s4 : subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4). @@ -1876,7 +1876,7 @@ End Subseq. Prenex Implicits subseq. Arguments subseqP {T s1 s2}. -Hint Resolve subseq_refl. +Hint Resolve subseq_refl : core. Section Rem. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index b8388f0..581a7ee 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -316,11 +316,11 @@ Lemma leq0n n : 0 <= n. Proof. by []. Qed. Lemma ltn0Sn n : 0 < n.+1. Proof. by []. Qed. Lemma ltn0 n : n < 0 = false. Proof. by []. Qed. Lemma leqnn n : n <= n. Proof. by elim: n. Qed. -Hint Resolve leqnn. +Hint Resolve leqnn : core. Lemma ltnSn n : n < n.+1. Proof. by []. Qed. Lemma eq_leq m n : m = n -> m <= n. Proof. by move->. Qed. Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed. -Hint Resolve leqnSn. +Hint Resolve leqnSn : core. Lemma leq_pred n : n.-1 <= n. Proof. by case: n => /=. Qed. Lemma leqSpred n : n <= n.-1.+1. Proof. by case: n => /=. Qed. @@ -344,7 +344,7 @@ Lemma lt0n n : (0 < n) = (n != 0). Proof. by case: n. Qed. Lemma lt0n_neq0 n : 0 < n -> n != 0. Proof. by case: n. Qed. Lemma eqn0Ngt n : (n == 0) = ~~ (n > 0). Proof. by case: n. Qed. Lemma neq0_lt0n n : (n == 0) = false -> 0 < n. Proof. by case: n. Qed. -Hint Resolve lt0n_neq0 neq0_lt0n. +Hint Resolve lt0n_neq0 neq0_lt0n : core. Lemma eqn_leq m n : (m == n) = (m <= n <= m). Proof. by elim: m n => [|m IHm] []. Qed. @@ -375,7 +375,7 @@ Proof. by move=> Hmn; apply: leq_trans. Qed. Lemma ltnW m n : m < n -> m <= n. Proof. exact: leq_trans. Qed. -Hint Resolve ltnW. +Hint Resolve ltnW : core. Lemma leqW m n : m <= n -> m <= n.+1. Proof. by move=> le_mn; apply: ltnW. Qed. |