adapt to MC#1256

Author: Tragicus

theories/algo_closures.v

@@ -46,9 +46,11 @@ Lemma d_Sn : annotated_recs_d.Sn d.
 Proof.
 rewrite /annotated_recs_d.Sn /annotated_recs_d.precond.Sn /d => n k m ?.
 rewrite addrAC !binSz /annotated_recs_d.Sn_cf0_0_0; [ | lia ..].
+field.
 have b1_pos: 0 < binomialz n m by apply: bin_nonneg; lia.
-have b2_pos: 0 < binomialz (n + m) m by apply: bin_nonneg; lia.
-by field; ring_lia.
+have ->: (binomialz (n + m) m)%:~R != 0 :> rat.
+  by rewrite intq_eq0; apply/Num.Theory.lt0r_neq0/bin_nonneg; lia.
+by ring_lia.
 Qed.
 
 (* This is a fake recurrence, because d does not really depend on k *)
@@ -63,9 +65,11 @@ Proof.
 rewrite /annotated_recs_d.Sm /annotated_recs_d.precond.Sm /d => n k m ?.
 rewrite int.zshiftP !alt_sign addrA !(binzS, binSz); [ | lia ..].
 rewrite /annotated_recs_d.Sm_cf0_0_0.
+field.
 have b1_pos: 0 < binomialz n m by apply: bin_nonneg; lia.
-have b2_pos: 0 < binomialz (n + m) m by apply: bin_nonneg; lia.
-by field; ring_lia.
+have ->: (binomialz (n + m) m)%:~R != 0 :> rat.
+  by rewrite intq_eq0; apply/Num.Theory.lt0r_neq0/bin_nonneg; lia.
+by ring_lia.
 Qed.
 
 Definition d_ann := annotated_recs_d.ann d_Sn d_Sk d_Sm.

theories/bigopz.v

@@ -240,7 +240,7 @@ Proof.
 suff -> : index_iotaz (m + a) n = map (fun i => i + a) (index_iotaz m (n - a)).
   by rewrite big_map.
 apply: (@eq_from_nth _ 0).
-  by rewrite size_map !size_index_iotaz lerBDl addrC -addrA opprD.
+  by rewrite size_map !size_index_iotaz lerBDl [m + a]addrC -addrA opprD.
 move=> i; rewrite size_index_iotaz; case: ifP => // hman hi.
 rewrite nth_index_iotaz // (nth_map 0); last first.
   rewrite size_index_iotaz lerBDr hman.
@@ -290,7 +290,7 @@ apply: (@eq_from_nth _ 0); rewrite size_cat !size_index_iotaz hmn hnp.
   have hmn' : `|n - m |  = n - m by apply: ger0_norm; rewrite subr_gte0.
   rewrite nth_index_iotaz //; last first.
     rewrite -subzn; last by  rewrite leqNgt hi2.
-    by rewrite lterBDr addrC h ltz_nat.
+    by rewrite lterBDr [ltRHS]addrC h ltz_nat.
   rewrite nth_index_iotaz //; last exact: le_trans hnp.
   rewrite -subzn; last by  rewrite leqNgt hi2.
   move: hmn'; rewrite abszE; move->. rewrite addrCA opprB.
@@ -311,7 +311,7 @@ Lemma big_int_recr m n F : m <= n ->
      op  (\big[op/idx]_(m <= i < n :> int) F (i)) (F n).
 Proof.
 move=> hmn; rewrite (@big_cat_int n) ?ler_wpDr //=.
-rewrite big_addz2l (@big_ltz 0 1) // add0r (@big_geqz 1 1) // add0r.
+rewrite big_addz2l (@big_ltz 0 1) // add0r (@big_geqz 1 1) // ?add0r.
 by rewrite Monoid.Theory.mulm1.
 Qed.
 

theories/multinomial.v

@@ -155,7 +155,7 @@ rewrite {}/s; elim/last_ind: l n m => [|l a ihl] n m /=.
 - move=> leqnm; rewrite size_rcons big_rcons /= exprDn.
   set s := size l.
   pose tlast s (t : s.-tuple 'I_m.+1) := last ord0 t.
-  have -> P F :
+  have -> P (F : _ -> R) :
    \sum_(t : s.+1.-tuple 'I_m.+1 | P t) F t =
    \sum_(j < m.+1) \sum_(t | P t && (tlast _ t == j)) F t.
      exact: partition_big.
@@ -171,7 +171,7 @@ rewrite {}/s; elim/last_ind: l n m => [|l a ihl] n m /=.
     by apply: (leq_trans (leq_subr _ _)); apply: (leq_trans leqnm).
   rewrite mulr_suml -sumrMnl.
   pose tsum a (t : a.-tuple 'I_m.+1) b := ((\sum_(j <- t) j) == b)%N.
-  have -> F :
+  have -> (F : _ -> R) :
   \sum_(t : s.+1.-tuple 'I_m.+1 | tsum _ t n && (tlast _ t == i)) F t =
   \sum_(t : s.-tuple 'I_m.+1    | tsum _ t (n - i)%N) F [tuple of (rcons t i)].
     pose indx (t : s.-tuple 'I_m.+1) := [tuple of rcons t i].

theories/posnum.v

@@ -46,7 +46,7 @@ Class infer (P : Prop) := Infer : P.
 Lemma inferP (P : Prop) : P -> infer P. Proof. by []. Qed.
 
 Lemma splitr (R : numFieldType) (x : R) : x = x / 2%:R + x / 2%:R.
-Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed.
+Proof. by rewrite -mulr2n -[RHS]mulr_natr mulfVK //= pnatr_eq0. Qed.
 
 Record posnum_def (R : numDomainType) := PosNumDef {
   num_of_pos :> R;