Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adapt to MC#1256 #62

Merged
merged 1 commit into from
Aug 6, 2024
+4 −3
Merged

adapt to MC#1256 #62

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/grid.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion theories/hubcap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 2 additions & 1 deletion theories/matte.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
Loading