search

coq-community / fav-ssr

Functional Algorithms Verified in SSReflect [maintainer=@clayrat]
MIT License
45 stars 7 forks source link

Use new inequality patterns #7

Open clayrat opened 2 years ago

clayrat commented 2 years ago

E.g., [X in (_ <= X)%N] becomes [leqRHS], see https://github.com/math-comp/math-comp/pull/869/