coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2019-11-22	New generalised induction idiom (#434)	Georges Gonthier
	Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using either new helper lemmas `ubnP` and `ltnSE` or a specific `nat` induction principle `ltn_ind`. Added (non-strict in)equality induction helper lemmas Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression along with some (in)equality, in preparation for some generalised induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed `ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember that the inductive value remains below the initial one. Used the change log to give notice to users to update the generalised induction idioms in their proofs to one of the new forms before Mathcomp 1.11.
2019-10-25	More arithmetic theorems	Cyril Cohen
	In ssrnat: - some trivial results in ssrnat `addnKC`, `ltn_predl`, `ltn_predr`, `ltn_subr` and `predn_sub` - theorems about `n <=/< p +/- m` and `m +/- n <=/< p` `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`, `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and `ltn_subCl` In div: - theorems about the euclidean division of additions and subtraction, + without preconditions of divisibility: `edivnD`, `edivnB`, `divnD`, `divnB`, `modnD`, `modnB` + with divisibility of one argument: `divnDMl`, `divnMBl`, `divnBMl`, `divnBl` and `divnBr` + specialization of the former theorems for .+1 and .-1: `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and `modn_pred`
2019-10-24	Added and generalized arithmetic theorems. (#394)	Cyril Cohen
	- Added: `modn_divl` and `divn_modl`. - Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
2019-05-08	suppress use of `Arith` hints	Sora Chen

2019-04-26	Cleaning Require and Require Imports	Cyril Cohen

2018-12-11	Fix some new warnings emitted by Coq 8.10:	Anton Trunov
	``` Warning: Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database. [implicit-core-hint-db,deprecated] ```
2018-11-21	Merge Arguments and Prenex Implicits	Anton Trunov
	See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
2018-07-12	Replace all the CoInductives with Variants	Kazuhiko Sakaguchi

2018-02-21	Change Implicit Arguments to Arguments in ssreflect	Jasper Hugunin

2018-02-06	running semi-automated linting on the whole library	Cyril Cohen

2016-11-07	update copyright banner	Assia Mahboubi

2016-02-09	[div] Move dvdn_fact from prime to div.	Emilio Jesus Gallego Arias

2015-11-05	merge basic/ into ssreflect/	Enrico Tassi