Merge pull request #62 from Tragicus/pr1256

adapt to MC#1256
coq-community · Aug 6, 2024 · c028f9b · c028f9b
2 parents 1efde3a + a361c3b
commit c028f9b
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/theories/grid.v b/theories/grid.v
@@ -355,7 +355,7 @@ Proof.
 rewrite -[xmax in RHS](subrK xmin) -ltrBlDr -subr_ge0 /zspan /zwidth.
 case: {xmax}(xmax - xmin) => n; last by case: (x - xmin).
 elim: n xmin => [|n IHn] x0; first by rewrite ltNge andbN.
-rewrite inE -subr_eq0 {}IHn opprD addrA lerBrDl ltrBlDl.
+rewrite inE -subr_eq0 {}IHn opprD addrA lerBrDl [in LHS]ltrBlDl.
 by rewrite orb_andr eq_sym -le_eqVlt; case: eqP => // <-.
 Qed.
 

diff --git a/theories/hubcap.v b/theories/hubcap.v
@@ -421,7 +421,7 @@ have [ltin | ?] := ltnP i nhub; last by rewrite Dvi nth_default ?Ev in vj_gt0.
 have [ltjn | ?] := ltnP j nhub; last by rewrite [vj]nth_default ?Ev in vj_gt0.
 rewrite !{}db2_inc -?Dvi {vb_hcij vb_hcj}//= addrA -lerBrDl -opprD -/vj.
 apply: {IHhc v_hc p_hc vb_hc}(le_trans (IHhc _ v_hc p_hc vb_hc)).
-rewrite lerN2 addrC lerD2r -mulrnDl ler_pMn2r //.
+rewrite lerN2 [leLHS]addrC lerD2r -mulrnDl ler_pMn2r //.
 rewrite addrC -(iter_hub_subn i ltjn) //.
 apply: check_2dbound2P p_b1; rewrite ?arity_iter_face ?hub_subn_hub //.
 by rewrite fit_hubcap_rot.

diff --git a/theories/matte.v b/theories/matte.v
@@ -245,7 +245,8 @@ case=> -> Dd; last rewrite -addrA subrK in Dd.
 suff Dd0: oddg d0 = oddg d by move: Dd; rewrite Dd0 => /addIr->; apply: map_f.
 have:= congr1 oddg Dd; rewrite oddg_add [RHS]oddg_add.
 have{r'E r_d0}: gedge d0 != d := hasPn r'E d0 r_d0.
-by rewrite /gedge 2!addrA -Dd -!addrA -subr_eq0 addrC addKr; do 2!case: oddgP.
+rewrite /gedge 2!addrA -Dd -!addrA -subr_eq0 [d + _ - d]addrC addKr.
+by do 2!case: oddgP.
 Qed.
 
 Lemma refine_mring_def : refine_mring (mring m) =i gborder (refine_mdisk m).