From a361c3bca6a73f83127b502c128d44617d340279 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 5 Aug 2024 13:48:03 +0200 Subject: [PATCH] adapt to MC#1256 --- theories/grid.v | 2 +- theories/hubcap.v | 2 +- theories/matte.v | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/theories/grid.v b/theories/grid.v index d07d27c..3b4c200 100644 --- 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 index 3f116f8..cac7168 100644 --- 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 index 8385021..87eb70e 100644 --- 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).